Adding an unshelve tactical.

This tactical is inspired by discussions on the Coq-club list. For now
it is still undocumented, and there is room left for design issues.

1 files changed, 10 insertions, 0 deletions

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 9ffcd2dcff..1355499e48 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -21,6 +21,7 @@ open Util
 open Evd
 open Equality
 open Misctypes
+open Proofview.Notations
 
 DECLARE PLUGIN "extratactics"
 
@@ -864,6 +865,15 @@ TACTIC EXTEND shelve_unifiable
     [ Proofview.shelve_unifiable ]
 END
 
+(* Unshelves the goal shelved by the tactic. *)
+TACTIC EXTEND unshelve
+| [ "unshelve" tactic(t) ] ->
+    [
+      Proofview.with_shelf (Tacinterp.eval_tactic t) >>= fun (gls, ()) ->
+      Proofview.Unsafe.tclNEWGOALS gls
+    ]
+END
+
 (* Command to add every unshelved variables to the focus *)
 VERNAC COMMAND EXTEND Unshelve
 [ "Unshelve" ]