Merge PR #13254: Adopt the same format for "Print Ltac foo" and "Print foo" when "foo" is an Ltac

Reviewed-by: ppedrot

5 files changed, 47 insertions, 44 deletions

diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index c38a4dcd90..c54f8ffa78 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -466,7 +466,7 @@ END
 
 VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY
 | [ "Print" "Ltac" reference(r) ] ->
-  { Feedback.msg_notice (Tacintern.print_ltac r) }
+  { Feedback.msg_notice (Tacentries.print_ltac r) }
 END
 
 VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index a05b36c1b4..29e29044f1 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -528,16 +528,40 @@ let print_ltacs () =
 
 let locatable_ltac = "Ltac"
 
+let split_ltac_fun = function
+  | Tacexpr.TacFun (l,t) -> (l,t)
+  | t -> ([],t)
+
+let pr_ltac_fun_arg n = spc () ++ Name.print n
+
+let print_ltac_body qid tac =
+  let filter mp =
+    try Some (Nametab.shortest_qualid_of_module mp)
+    with Not_found -> None
+  in
+  let mods = List.map_filter filter tac.Tacenv.tac_redef in
+  let redefined = match mods with
+  | [] -> mt ()
+  | mods ->
+    let redef = prlist_with_sep fnl pr_qualid mods in
+    fnl () ++ str "Redefined by:" ++ fnl () ++ redef
+  in
+  let l,t = split_ltac_fun tac.Tacenv.tac_body in
+  hv 2 (
+    hov 2 (str "Ltac" ++ spc() ++ pr_qualid qid ++
+           prlist pr_ltac_fun_arg l ++ spc () ++ str ":=")
+    ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined
+
 let () =
   let open Prettyp in
-  let locate qid = try Some (Tacenv.locate_tactic qid) with Not_found -> None in
-  let locate_all = Tacenv.locate_extended_all_tactic in
-  let shortest_qualid = Tacenv.shortest_qualid_of_tactic in
-  let name kn = str "Ltac" ++ spc () ++ pr_path (Tacenv.path_of_tactic kn) in
-  let print kn =
-    let qid = qualid_of_path (Tacenv.path_of_tactic kn) in
-    Tacintern.print_ltac qid
-  in
+  let locate qid = try Some (qid, Tacenv.locate_tactic qid) with Not_found -> None in
+  let locate_all qid = List.map (fun kn -> (qid,kn)) (Tacenv.locate_extended_all_tactic qid) in
+  let shortest_qualid (qid,kn) = Tacenv.shortest_qualid_of_tactic kn in
+  let name (qid,kn) = str "Ltac" ++ spc () ++ pr_path (Tacenv.path_of_tactic kn) in
+  let print (qid,kn) =
+    let entries = Tacenv.ltac_entries () in
+    let tac = KNmap.find kn entries in
+    print_ltac_body qid tac in
   let about = name in
   register_locatable locatable_ltac {
     locate;
@@ -551,6 +575,17 @@ let () =
 let print_located_tactic qid =
   Feedback.msg_notice (Prettyp.print_located_other locatable_ltac qid)
 
+let print_ltac id =
+ try
+  let kn = Tacenv.locate_tactic id in
+  let entries = Tacenv.ltac_entries () in
+  let tac = KNmap.find kn entries in
+  print_ltac_body id tac
+ with
+  Not_found ->
+   user_err ~hdr:"print_ltac"
+    (pr_qualid id ++ spc() ++ str "is not a user defined tactic.")
+
 (** Grammar *)
 
 let () =
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 6ee3ce091b..fc9ab54eba 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -69,6 +69,9 @@ val print_ltacs : unit -> unit
 val print_located_tactic : Libnames.qualid -> unit
 (** Display the absolute name of a tactic. *)
 
+val print_ltac : Libnames.qualid -> Pp.t
+(** Display the definition of a tactic. *)
+
 (** {5 Low-level registering of tactics} *)
 
 type (_, 'a) ml_ty_sig =
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 9c3b05fdf1..47f1d3bf66 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -769,38 +769,6 @@ let glob_tactic_env l env x =
   (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars })
     x
 
-let split_ltac_fun = function
-  | TacFun (l,t) -> (l,t)
-  | t -> ([],t)
-
-let pr_ltac_fun_arg n = spc () ++ Name.print n
-
-let print_ltac id =
- try
-  let kn = Tacenv.locate_tactic id in
-  let entries = Tacenv.ltac_entries () in
-  let tac = KNmap.find kn entries in
-  let filter mp =
-    try Some (Nametab.shortest_qualid_of_module mp)
-    with Not_found -> None
-  in
-  let mods = List.map_filter filter tac.Tacenv.tac_redef in
-  let redefined = match mods with
-  | [] -> mt ()
-  | mods ->
-    let redef = prlist_with_sep fnl pr_qualid mods in
-    fnl () ++ str "Redefined by:" ++ fnl () ++ redef
-  in
-  let l,t = split_ltac_fun tac.Tacenv.tac_body in
-  hv 2 (
-    hov 2 (str "Ltac" ++ spc() ++ pr_qualid id ++
-           prlist pr_ltac_fun_arg l ++ spc () ++ str ":=")
-    ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined
- with
-  Not_found ->
-   user_err ~hdr:"print_ltac"
-    (pr_qualid id ++ spc() ++ str "is not a user defined tactic.")
-
 (** Registering *)
 
 let lift intern = (); fun ist x -> (ist, intern ist x)
diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli
index 22ec15566b..f779aa470c 100644
--- a/plugins/ltac/tacintern.mli
+++ b/plugins/ltac/tacintern.mli
@@ -55,9 +55,6 @@ val intern_hyp : glob_sign -> lident -> lident
 
 val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument
 
-(** printing *)
-val print_ltac : Libnames.qualid -> Pp.t
-
 (** Reduction expressions *)
 
 val intern_red_expr : glob_sign -> raw_red_expr -> glob_red_expr