diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-09 11:56:52 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-12-09 11:57:07 +0100 |
| commit | 8ea758fbb392e270e6a8d2287dbb5b0455d99368 (patch) | |
| tree | c024c0fe2548ab03af2aa96c4f45594d520551af /tactics | |
| parent | 5c5b5906426f38323fc5d63f4dc634672ebd2649 (diff) | |
Fixing parsing of the unshelve tactical.
Now [unshelve tac1; tac2] is parsed as [(unshelve tac1); tac2].
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 1355499e4..827d2e25a 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 |