From 5b92ff7b0a641bf2daa31b60bf49b57a5d1e8452 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack <arnaud@spiwack.net>
Date: Tue, 5 Aug 2014 16:08:29 +0200
Subject: Ltac's idtac is now implemented using the new API.

---
 tactics/tacinterp.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'tactics/tacinterp.ml')

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index b8557e3d3..4b0bf1fae 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) ->
-- 
cgit v1.2.3