diff options
| -rw-r--r-- | tactics/extratactics.ml4 | 5 |
1 files 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 |