fix: losing postponed universe constraints

This bug was exposed by #342
2021-03-10 14:18:03 -08:00 · 2021-03-10 14:18:03 -08:00 · 847f95021a
commit 847f95021a
parent 904c23e901
1 changed files with 2 additions and 0 deletions
--- 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