From 8ea758fbb392e270e6a8d2287dbb5b0455d99368 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 9 Dec 2015 11:56:52 +0100
Subject: Fixing parsing of the unshelve tactical.

Now [unshelve tac1; tac2] is parsed as [(unshelve tac1); tac2].
---
 tactics/extratactics.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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