Re-add printer for tacdef_body so that Ltac definitions are printed by pr_vernac.

1 files changed, 19 insertions, 0 deletions

diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index b55ac9ad0..c264b1906 100644
--- a/ltac/g_ltac.ml4
+++ b/ltac/g_ltac.ml4
@@ -413,7 +413,26 @@ VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY
   [ msg_notice (Tacintern.print_ltac (snd (Libnames.qualid_of_reference r))) ]
 END
 
+let pr_ltac_ref = Libnames.pr_reference
+
+let pr_tacdef_body tacdef_body =
+  let id, redef, body =
+    match tacdef_body with
+    | TacticDefinition ((_,id), body) -> Nameops.pr_id id, false, body
+    | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body
+  in
+  let idl, body =
+    match body with
+      | Tacexpr.TacFun (idl,b) -> idl,b
+      | _ -> [], body in
+  id ++
+    prlist (function None -> str " _"
+      | Some id -> spc () ++ Nameops.pr_id id) idl
+  ++ (if redef then str" ::=" else str" :=") ++ brk(1,1)
+  ++ Pptactic.pr_raw_tactic body
+
 VERNAC ARGUMENT EXTEND ltac_tacdef_body
+PRINTED BY pr_tacdef_body
 | [ tacdef_body(t) ] -> [ t ]
 END