diff options
| author | Arnaud Spiwack | 2014-08-05 16:08:29 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-08-05 16:52:14 +0200 |
| commit | 5b92ff7b0a641bf2daa31b60bf49b57a5d1e8452 (patch) | |
| tree | 62d40878d0dbca6404750c5fd699f63d031032e7 | |
| parent | 4eaafcd00992302c186b8d11e890616726ebd822 (diff) | |
Ltac's idtac is now implemented using the new API.
| -rw-r--r-- | tactics/tacinterp.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index b8557e3d35..4b0bf1faed 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1048,8 +1048,13 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with | TacMatchGoal _ | TacMatch _ -> assert false | TacId s -> Proofview.tclTHEN - (Proofview.V82.tactic begin fun gl -> - tclIDTAC_MESSAGE (interp_message_nl ist (pf_env gl) s) gl + (Proofview.Goal.enter begin fun gl -> + let msg = + try Proofview.tclUNIT (interp_message_nl ist (Proofview.Goal.env gl) 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 (db_breakpoint (curr_debug ist) s)) | TacFail (n,s) -> |