fix: reorder goals after specialize (#1796)

* fix: reorder goals after specialize * fix test
leanprover · Nov 3, 2022 · d0dc9a2 · d0dc9a2
1 parent 5249611
commit d0dc9a2
Show file tree

Hide file tree

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