Print [rename] tactic properly in info trace.

Followup of d0a871374e3b3498c51d9d7b8e4510f7e1e7a3e1 (Writing rename_hyps in the new monad).

1 files changed, 8 insertions, 6 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index dd9816eaf..b320e9bb1 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 *)