From 41af4c3e36af15d9cc235cb5effedeed40478d2e Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 9 Apr 2016 16:30:48 +0200
Subject: Re-add printer for tacdef_body so that Ltac definitions are printed
 by pr_vernac.

---
 ltac/g_ltac.ml4 | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/ltac/g_ltac.ml4 b/ltac/g_ltac.ml4
index b55ac9ad06..c264b19063 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
 
-- 
cgit v1.2.3