From a6fa936bbd0c4367b7a4d87df786645c138327b3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 27 Apr 2016 22:13:04 +0200
Subject: Revert "Honor parsing and printing levels for tactic entry in TACTIC
 EXTEND and"

This reverts commit c4ce1baa9f66210ebc1909988b3dd8baa1b8ef27.
---
 printing/pptactic.ml | 26 +-------------------------
 1 file changed, 1 insertion(+), 25 deletions(-)

(limited to 'printing')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 06bf077419..5dbf9a42a3 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1390,33 +1390,9 @@ let () =
   Genprint.register_print0 Stdarg.wit_pre_ident str str str;
   Genprint.register_print0 Stdarg.wit_string pr_string pr_string pr_string
 
-let () =
-  let printer _ _ prtac = prtac (5, E) in
-  declare_extra_genarg_pprule wit_tactic printer printer printer
-
 let () =
   let printer _ _ prtac = prtac (0, E) in
-  declare_extra_genarg_pprule wit_tactic0 printer printer printer
-
-let () =
-  let printer _ _ prtac = prtac (1, E) in
-  declare_extra_genarg_pprule wit_tactic1 printer printer printer
-
-let () =
-  let printer _ _ prtac = prtac (2, E) in
-  declare_extra_genarg_pprule wit_tactic2 printer printer printer
-
-let () =
-  let printer _ _ prtac = prtac (3, E) in
-  declare_extra_genarg_pprule wit_tactic3 printer printer printer
-
-let () =
-  let printer _ _ prtac = prtac (4, E) in
-  declare_extra_genarg_pprule wit_tactic4 printer printer printer
-
-let () =
-  let printer _ _ prtac = prtac (5, E) in
-  declare_extra_genarg_pprule wit_tactic5 printer printer printer
+  declare_extra_genarg_pprule wit_tactic printer printer printer
 
 let () =
   let pr_unit _ _ _ () = str "()" in
-- 
cgit v1.2.3