fix: resumePostponed backtracking

Note that test for issue #1200 broke.
The bug fixed by this commit was allowing the example to be elaborated
correctly :(
Initially, the type of the discriminant is not available, and
`.none (α:=α)` can only be elaborated when the expected type is of the
form `C ...`. Lean then tries to elaborate the alternatives, learn
that the discriminant should be `Option ?m`, and fails because the
patterns still have metavariables after elaboration. Before the bug
fix, `resumePostpone` was **not** restoring the metavariable context,
and the assingnment would stay there. With this information, Lean
can now elaborate `.none (α:=α)`.
Although the bug had a positive impact in this case, it produced
incorrect behavior in other examples.
The fixed example looks reasonable. Thus, we will not reopen
issue #1200

src/Lean/Elab/SyntheticMVars.lean

@@ -23,7 +23,7 @@ private def resumeElabTerm (stx : Syntax) (expectedType? : Option Expr) (errToSo
   It is used to implement `synthesizeSyntheticMVars`. -/
 private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId : MVarId) (postponeOnError : Bool) : TermElabM Bool :=
   withRef stx <| withMVarContext mvarId do
-    let s ← get
+    let s ← saveState
     try
       withSavedContext savedContext do
         let mvarDecl     ← getMVarDecl mvarId
@@ -42,13 +42,13 @@ private def resumePostponed (savedContext : SavedContext) (stx : Syntax) (mvarId
     catch
      | ex@(.internal id _) =>
        if id == postponeExceptionId then
-         set s
+         s.restore (restoreInfo := true)
          return false
        else
          throw ex
      | ex@(.error ..) =>
        if postponeOnError then
-         set s
+         s.restore (restoreInfo := true)
          return false
        else
          logException ex

tests/lean/run/1200.lean

@@ -1,5 +1,5 @@
 example
-(h: match .none (α:=α) with
+(h: match none (α:=α) with
 | some _ => True
 | _      => True):
   True := by