diff options
| author | Pierre-Marie Pédrot | 2014-09-04 12:09:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-09-04 12:57:33 +0200 |
| commit | a8a0cd9d5cf849be3b995ffc19e2cb4a0ff33d7a (patch) | |
| tree | 30ef0390ec873bb50914f3196e9af74d48cb5719 /tactics/tacinterp.ml | |
| parent | ba9ba59be9534b42ede74adfcbf8b85b876590c7 (diff) | |
Revert "Ltac's idtac is now implemented using the new API."
This reverts commit 5b92ff7b0a641bf2daa31b60bf49b57a5d1e8452.
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index df79361feb..cc1dcb4536 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1102,13 +1102,8 @@ 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 -> - 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)) + (Proofview.V82.tactic begin fun gl -> + tclIDTAC_MESSAGE (interp_message_nl ist (pf_env gl) s) gl end) (Proofview.tclLIFT (db_breakpoint (curr_debug ist) s)) | TacFail (n,s) -> |