From cb6f036b8e097085a849f806aa7c2627b789bd1f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 13 Apr 2016 21:53:40 +0200
Subject: Fixing printing of Function.

---
 plugins/funind/g_indfun.ml4 | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'plugins')

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index e93c395e3d..0760e78bff 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -164,6 +164,11 @@ GEXTEND Gram
 
 END
 
+let () =
+  let raw_printer _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in
+  let printer _ _ _ _ = str "<Unavailable printer for rec_definition>" in
+  Pptactic.declare_extra_genarg_pprule wit_function_rec_definition_loc raw_printer printer printer
+
 (* TASSI: n'importe quoi ! *)
 VERNAC COMMAND EXTEND Function
    ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
-- 
cgit v1.2.3