Info: Tactics coming from [TACTIC EXTEND] print their names.

Since PMP's intervention, the [TACTIC EXTEND] tactics are not uniform: some are syntax, and some are just an internal name for an Ltac definition. The latter kind prints an internal name. It may be better to avoid printing them in the trace altogether. But I haven't figured out how to detect that properly yet.

1 files changed, 6 insertions, 2 deletions

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3e96ae1f58..a726253dc8 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1244,7 +1244,9 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       let goal = Evar.unsafe_of_int (-1) in
       (* /dummy values *)
       let args = List.map (fun a -> snd(interp_genarg ist env sigma concl goal a)) l in
-      catch_error_tac trace (tac args ist)
+      let name () = Pptactic.pr_tactic env (TacML(loc,opn,args)) in
+      Proofview.Trace.name_tactic name
+        (catch_error_tac trace (tac args ist))
   | TacML (loc,opn,l) ->
       let trace = push_trace (loc,LtacMLCall tac) ist in
       let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in
@@ -1259,7 +1261,9 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
             (fun a sigma -> interp_genarg ist env sigma concl goal a) l goal_sigma
         in
         Proofview.Unsafe.tclEVARS sigma <*>
-        catch_error_tac trace (tac args ist)
+        let name () = Pptactic.pr_tactic env (TacML(loc,opn,args)) in
+        Proofview.Trace.name_tactic name
+          (catch_error_tac trace (tac args ist))
       end
 
 and force_vrec ist v : typed_generic_argument Ftactic.t =