diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-05 16:13:33 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-08-05 16:56:20 +0200 |
| commit | afa441019432f70245fed6adc5eb0318514e4357 (patch) | |
| tree | 822bf107f1e1b7dec8a6857e086e6f2996b67b96 /tactics | |
| parent | 5b92ff7b0a641bf2daa31b60bf49b57a5d1e8452 (diff) | |
Ltac's [idtac] is now interpreted outside of a goal if possible.
It avoids printing several times the same things when no constr are involved in the message. It also allows to print messages even after all goals have been solved.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacinterp.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 4b0bf1fae..e0d24e9e1 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1048,14 +1048,13 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacMatchGoal _ | TacMatch _ -> assert false | TacId s -> Proofview.tclTHEN - (Proofview.Goal.enter begin fun gl -> + (Proofview.tclENV >>= fun env -> let msg = - try Proofview.tclUNIT (interp_message_nl ist (Proofview.Goal.env gl) s) + try Proofview.tclUNIT (interp_message_nl ist env s) with e when Errors.noncritical e -> Proofview.tclZERO e in msg >>= fun msg -> - Proofview.tclLIFT (Proofview.NonLogical.print (Pp.hov 0 msg)) - end) + Proofview.tclLIFT (Proofview.NonLogical.print (Pp.hov 0 msg))) (Proofview.tclLIFT (db_breakpoint (curr_debug ist) s)) | TacFail (n,s) -> Proofview.V82.tactic begin fun gl -> |