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(-)

(limited to 'tactics')

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


From cedcfc9bc386456f3fdd225f739706e4f7a2902c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 15 Dec 2015 10:51:08 +0100
Subject: Refine tactic now shelves unifiable holes.

The unshelve tactical can be used to get the shelved holes. This changes the
proper ordering of holes though, so expect some broken scripts. Also, the
test-suite is not fixed yet.
---
 tactics/extratactics.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 35efb0b657..ca65f08ec0 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -357,7 +357,7 @@ let refine_tac {Glob_term.closure=closure;term=term} =
       Pretyping.ltac_idents = closure.Glob_term.idents;
     } in
     let update evd = Pretyping.understand_ltac flags env evd lvar tycon term in
-    Tactics.New.refine ~unsafe:false update
+    Tactics.New.refine ~unsafe:false update <*> Proofview.shelve_unifiable
   end
 
 TACTIC EXTEND refine
-- 
cgit v1.2.3


From b8d1e84e9326df34383e5e5c8c5842cb7013b935 Mon Sep 17 00:00:00 2001
From: Guillaume Melquiond
Date: Wed, 16 Dec 2015 18:30:32 +0100
Subject: Add a "simple refine" variant of "refine" that does not call
 "shelve_unifiable".

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

(limited to 'tactics')

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ca65f08ec0..e06997029d 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -345,7 +345,7 @@ END
 (**********************************************************************)
 (* Refine                                                             *)
 
-let refine_tac {Glob_term.closure=closure;term=term} =
+let refine_tac simple {Glob_term.closure=closure;term=term} =
   Proofview.Goal.nf_enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
@@ -357,11 +357,16 @@ let refine_tac {Glob_term.closure=closure;term=term} =
       Pretyping.ltac_idents = closure.Glob_term.idents;
     } in
     let update evd = Pretyping.understand_ltac flags env evd lvar tycon term in
-    Tactics.New.refine ~unsafe:false update <*> Proofview.shelve_unifiable
+    let refine = Proofview.Refine.refine ~unsafe:false update in
+    if simple then refine
+    else refine <*>
+           Tactics.New.reduce_after_refine <*>
+           Proofview.shelve_unifiable
   end
 
 TACTIC EXTEND refine
-  [ "refine" uconstr(c) ] -> [  refine_tac c ]
+| [ "refine" uconstr(c) ] -> [ refine_tac false c ]
+| [ "simple" "refine" uconstr(c) ] -> [ refine_tac true c ]
 END
 
 (**********************************************************************)
-- 
cgit v1.2.3


From 793cf771e18be3d44d3fcf89998dec50fb8229f3 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Wed, 16 Dec 2015 21:33:03 +0100
Subject: FIx parsing of tactic "simple refine".

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

(limited to 'tactics')

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index e06997029d..1d594aa7c9 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -366,6 +366,9 @@ let refine_tac simple {Glob_term.closure=closure;term=term} =
 
 TACTIC EXTEND refine
 | [ "refine" uconstr(c) ] -> [ refine_tac false c ]
+END
+
+TACTIC EXTEND simple_refine
 | [ "simple" "refine" uconstr(c) ] -> [ refine_tac true c ]
 END
 
-- 
cgit v1.2.3