fix: reorder goals after specialize (leanprover#1796)

* fix: reorder goals after specialize * fix test
digama0 · Nov 30, 2022 · a808286 · a808286
1 parent f86c13e
commit a808286
Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -174,7 +174,7 @@ def refineCore (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool) : Ta
       let mvarId ← (← getMainGoal).assert localDecl.userName (← inferType e).headBeta e
       let (_, mvarId) ← mvarId.intro1P
       let mvarId ← mvarId.tryClear h.fvarId!
-      replaceMainGoal (mvarId :: mvarIds')
+      replaceMainGoal (mvarIds' ++ [mvarId])
     else
       throwError "'specialize' requires a term of the form `h x_1 .. x_n` where `h` appears in the local context"
   | _ => throwUnsupportedSyntax

diff --git a/tests/lean/run/specialize1.lean b/tests/lean/run/specialize1.lean
@@ -20,9 +20,9 @@ example (X : Type) [Add X] (f : forall {A : Type} [Add A], A → A → A) (x : X
 
 def ex (f : Nat → Nat → Nat) : Nat := by
   specialize f _ _
-  exact f
   exact 10
   exact 2
+  exact f
 
 example : ex (· - ·) = 8 :=
   rfl