From 8b15e47a6b3ccae696da8e12dbad81ae0a740782 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 15 Dec 2015 11:25:54 +0100
Subject: Changing the order of the goals generated by unshelve.

---
 tactics/extratactics.ml4 | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 827d2e25a6..35efb0b657 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -867,10 +867,11 @@ END
 
 (* Unshelves the goal shelved by the tactic. *)
 TACTIC EXTEND unshelve
-| [ "unshelve" tactic0(t) ] ->
+| [ "unshelve" tactic1(t) ] ->
     [
       Proofview.with_shelf (Tacinterp.eval_tactic t) >>= fun (gls, ()) ->
-      Proofview.Unsafe.tclNEWGOALS gls
+      Proofview.Unsafe.tclGETGOALS >>= fun ogls ->
+      Proofview.Unsafe.tclSETGOALS (gls @ ogls)
     ]
 END
 
-- 
cgit v1.2.3