From dcc2283426fa760e078dff96e2e1de888991917e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 15 Jan 2021 17:03:40 -0800
Subject: [PATCH] fix: `refineCore`

closes #269
---
 src/Lean/Elab/Tactic/ElabTerm.lean |  2 +-
 tests/lean/run/269.lean            | 15 +++++++++++++++
 2 files changed, 16 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/269.lean

diff --git a/src/Lean/Elab/Tactic/ElabTerm.lean b/src/Lean/Elab/Tactic/ElabTerm.lean
index f6080f6dfe..4a71e6660a 100644
--- a/src/Lean/Elab/Tactic/ElabTerm.lean
+++ b/src/Lean/Elab/Tactic/ElabTerm.lean
@@ -63,7 +63,7 @@ def refineCore (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool) : Ta
     let decl ← getMVarDecl g
     let (val, gs') ← elabTermWithHoles stx decl.type tagSuffix allowNaturalHoles
     assignExprMVar g val
-    setGoals (gs ++ gs')
+    setGoals (gs' ++ gs)
 
 @[builtinTactic «refine»] def evalRefine : Tactic := fun stx =>
   match stx with
diff --git a/tests/lean/run/269.lean b/tests/lean/run/269.lean
new file mode 100644
index 0000000000..e4cf1999df
--- /dev/null
+++ b/tests/lean/run/269.lean
@@ -0,0 +1,15 @@
+theorem haveWithSubgoals {a b : α} : a = b ↔ b = a := by
+    apply Iff.intro
+    intro h
+    have h' := h.symm
+    exact h'
+    intro h
+    exact h.symm
+
+theorem haveWithSubgoals2 {a b : α} : a = b ↔ b = a := by {
+    apply Iff.intro;
+    intro h;
+    have h' := h.symm;
+    exact h';
+    intro h; exact h.symm;
+}