From 2c72ba5cb6864936067dd23cc40e28fe82f14ec5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 27 Apr 2016 22:13:03 +0200
Subject: Revert "Fixing printing of Function."

This reverts commit cb6f036b8e097085a849f806aa7c2627b789bd1f.
---
 plugins/funind/g_indfun.ml4 | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 0760e78bf..e93c395e3 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -164,11 +164,6 @@ 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