From 18046e2525300b990db4c8817f1cc02dcab97445 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 1 Sep 2016 09:59:20 +0200
Subject: Moving log of "TacReduce"/"reduce" to Tactics.reduce so that internal
 calls are logged too. Using appropriate printer for reparsability of the
 output.

---
 ltac/tacinterp.ml  | 3 ---
 tactics/tactics.ml | 7 +++++--
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml
index 397cd988da..83d67c8e32 100644
--- a/ltac/tacinterp.ml
+++ b/ltac/tacinterp.ml
@@ -1822,13 +1822,10 @@ and interp_atomic ist tac : unit Proofview.tactic =
 
   (* Conversion *)
   | TacReduce (r,cl) ->
-      (* spiwack: until the tactic is in the monad *)
-      Proofview.Trace.name_tactic (fun () -> Pp.str"<reduce>") begin
       Proofview.Goal.nf_s_enter { s_enter = begin fun gl ->
         let (sigma,r_interp) = interp_red_expr ist (pf_env gl) (project gl) r in
         Sigma.Unsafe.of_pair (Tactics.reduce r_interp (interp_clause ist (pf_env gl) (project gl) cl), sigma)
       end }
-      end
   | TacChange (None,c,cl) ->
       (* spiwack: until the tactic is in the monad *)
       Proofview.Trace.name_tactic (fun () -> Pp.str"<change>") begin
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index acc0fa1ca7..c9cec828c1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -869,14 +869,17 @@ let reduction_clause redexp cl =
 	(None, bind_red_expr_occurrences occs nbcl redexp)) cl
 
 let reduce redexp cl =
+  let trace () = Pp.(hov 2 (Pptactic.pr_atomic_tactic (Global.env()) (TacReduce (redexp,cl)))) in
+  Proofview.Trace.name_tactic trace begin
   Proofview.Goal.enter { enter = begin fun gl ->
-  let cl = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in
-  let redexps = reduction_clause redexp cl in
+  let cl' = concrete_clause_of (fun () -> Tacmach.New.pf_ids_of_hyps gl) cl in
+  let redexps = reduction_clause redexp cl' in
   let check = match redexp with Fold _ | Pattern _ -> true | _ -> false in
   Tacticals.New.tclMAP (fun (where,redexp) ->
     e_reduct_option ~check
       (Redexpr.reduction_of_red_expr (Tacmach.New.pf_env gl) redexp) where) redexps
   end }
+  end
 
 (* Unfolding occurrences of a constant *)
 
-- 
cgit v1.2.3