From a808286c7eac0a738b22e91525d889c7d2cd32fb Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Fri, 4 Nov 2022 00:32:55 +1100
Subject: [PATCH] fix: reorder goals after specialize (#1796)

* fix: reorder goals after specialize

* fix test
---
 src/Lean/Elab/Tactic/ElabTerm.lean | 2 +-
 tests/lean/run/specialize1.lean    | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index dacbeabeae6b6..3c1a7f8ad3ea2 100644
--- 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
index 8f473d397a871..e2103598643f2 100644
--- 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