From 847f95021aea1794f3569723bda46c13c3eb0ff1 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 10 Mar 2021 14:18:03 -0800
Subject: [PATCH] fix: losing postponed universe constraints

This bug was exposed by #342
---
 src/Lean/Meta/LevelDefEq.lean | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/Lean/Meta/LevelDefEq.lean b/src/Lean/Meta/LevelDefEq.lean
index 3cbcca9e7d..1fbd04128c 100644
--- a/src/Lean/Meta/LevelDefEq.lean
+++ b/src/Lean/Meta/LevelDefEq.lean
@@ -213,6 +213,8 @@ private def restore (env : Environment) (mctx : MetavarContext) (postponed : Per
   try
     if (← x) then
       if (← processPostponed mayPostpone) then
+        let newPostponed ← getPostponed
+        setPostponed (postponed ++ newPostponed)
         return true
       else
         restore env mctx postponed