Use same code for "Print Ltac foo" and "Print foo" when "foo" is an Ltac.

Adopting the same format means printing "Ltac foo := ..." and not the
fully qualified name of foo.

1 files changed, 43 insertions, 8 deletions

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 () =