Info: print a name for the primitive tactics in [Proofview].

The name is chosen in accordance to Ltac's syntax. In particular [refine] prints as Ltac's refine, which is not entirely correct (Ltac's refine does some βι-reduction after refinement). Maybe it would be better to give make it clear that it is a different refine. Still in refine, the constr is printed without taking into account the new evars, which, apart from potentially getting the order of the goals wrong, prints new evars as ?x instead of ?[x]. A printer for terms with new evars will be necessary.

In the case of [V82.tactic], the name is just <unknown> because there is no way to retrieve any information. It won't appear in the first level of info in Ltac, however, if the user would require a deeper trace, he may see internal tactics (Tactics defined with TACTIC EXTEND also have weird, unparsable, internal names).

3 files changed, 20 insertions, 0 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index 75cce2755a..1880d90ee9 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -51,6 +51,7 @@ let pr_lconstr_core goal_concl_style env sigma t =
 
 let pr_lconstr_env env = pr_lconstr_core false env
 let pr_constr_env env = pr_constr_core false env
+let _ = Hook.set Proofview.Refine.pr_constr pr_constr_env
 
 let pr_lconstr_goal_style_env env = pr_lconstr_core true env
 let pr_constr_goal_style_env env = pr_constr_core true env
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index e03249ca56..ba61bf7a5f 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -533,6 +533,7 @@ let shelve =
   let open Proof in
   Comb.get >>= fun initial ->
   Comb.set [] >>
+  InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve")) >>
   Shelf.put initial
 
 
@@ -571,6 +572,7 @@ let shelve_unifiable =
   Pv.get >>= fun initial ->
   let (u,n) = partition_unifiable initial.solution initial.comb in
   Comb.set n >>
+  InfoL.leaf (Info.Tactic (fun () -> Pp.str"shelve_unifiable")) >>
   Shelf.put u
 
 (** [guard_no_unifiable] fails with error [UnresolvedBindings] if some
@@ -604,6 +606,8 @@ let goodmod p m =
   if p' < 0 then p'+m else p'
 
 let cycle n =
+  let open Proof in
+  InfoL.leaf (Info.Tactic (fun () -> Pp.(str"cycle"++spc()++int n))) >>
   Comb.modify begin fun initial ->
     let l = CList.length initial in
     let n' = goodmod n l in
@@ -612,6 +616,8 @@ let cycle n =
   end
 
 let swap i j =
+  let open Proof in
+  InfoL.leaf (Info.Tactic (fun () -> Pp.(str"swap"++spc()++int i++spc()++int j))) >>
   Comb.modify begin fun initial ->
     let l = CList.length initial in
     let i = if i>0 then i-1 else i and j = if j>0 then j-1 else j in
@@ -625,6 +631,8 @@ let swap i j =
   end
 
 let revgoals =
+  let open Proof in
+  InfoL.leaf (Info.Tactic (fun () -> Pp.str"revgoals")) >>
   Comb.modify CList.rev
 
 let numgoals =
@@ -663,6 +671,7 @@ let give_up =
   Comb.get >>= fun initial ->
   Comb.set [] >>
   mark_as_unsafe >>
+  InfoL.leaf (Info.Tactic (fun () -> Pp.str"give_up")) >>
   Giveup.put initial
 
 
@@ -920,6 +929,9 @@ struct
     let () = Typing.check env evdref c concl in
     !evdref
 
+  let (pr_constrv,pr_constr) =
+    Hook.make ~default:(fun _env _sigma _c -> Pp.str"<constr>") ()
+
   let refine ?(unsafe = false) f = Goal.enter begin fun gl ->
     let sigma = Goal.sigma gl in
     let env = Goal.env gl in
@@ -949,6 +961,8 @@ struct
     (** Select the goals *)
     let comb = undefined sigma (CList.rev evs) in
     let sigma = CList.fold_left mark_as_goal sigma comb in
+    let open Proof in
+    InfoL.leaf (Info.Tactic (fun () -> Pp.(str"refine"++spc()++ Hook.get pr_constrv env sigma c))) >>
     Pv.set { solution = sigma; comb; }
   end
 
@@ -1024,6 +1038,7 @@ module V82 = struct
       in
       let (goalss,evd) = Evd.Monad.List.map tac initgoals initevd in
       let sgs = CList.flatten goalss in
+      InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >>
       Pv.set { solution = evd; comb = sgs; }
     with e when catchable_exception e ->
       let e = Errors.push e in
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index cc8706ab2e..52b9d3c11a 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -450,6 +450,10 @@ end
 
 module Refine : sig
 
+  (** Printer used to print the constr which refine refines. *)
+  val pr_constr :
+    (Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds) Hook.t
+
   (** {7 Refinement primitives} *)
 
   val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * Constr.t) -> unit tactic