From afa441019432f70245fed6adc5eb0318514e4357 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 5 Aug 2014 16:13:33 +0200
Subject: 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.
---
 tactics/tacinterp.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

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