From b320666d84e2f9b91d0ab6dd70f29cdb7da68818 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 7 Nov 2014 09:10:07 +0100
Subject: Print [rename] tactic properly in info trace.

Followup of d0a871374e3b3498c51d9d7b8e4510f7e1e7a3e1 (Writing rename_hyps in the new monad).---
 tactics/tacinterp.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index dd9816eafd..b320e9bb16 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2032,15 +2032,17 @@ and interp_atomic ist tac : unit Proofview.tactic =
                    gl
       end
   | TacRename l ->
-      (* spiwack: until the tactic is in the monad *)
-      Proofview.Trace.name_tactic (fun () -> Pp.str"<rename>") begin
       Proofview.Goal.enter begin fun gl ->
         let env = Tacmach.New.pf_env gl in
         let sigma = Proofview.Goal.sigma gl in
-        Tactics.rename_hyp (List.map (fun (id1,id2) ->
-	  interp_hyp ist env sigma id1,
-	  interp_fresh_ident ist env sigma (snd id2)) l)
-      end
+        let l =
+          List.map (fun (id1,id2) ->
+	    interp_hyp ist env sigma id1,
+	    interp_fresh_ident ist env sigma (snd id2)) l
+        in
+        name_atomic ~env
+          (TacRename l)
+          (Tactics.rename_hyp l)
       end
 
   (* Constructors *)
-- 
cgit v1.2.3