From eb9216e544cb5fce4347052f42e9452a822c2f64 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 26 Apr 2016 12:17:42 +0200
Subject: Revert "Honor parsing and printing levels for tactic entry in TACTIC
 EXTEND and"

This reverts commit fb1b7b084bcbbbc176040fcadeac00aee6b1e462.
---
 interp/constrarg.ml  | 18 ------------------
 interp/constrarg.mli | 12 ------------
 2 files changed, 30 deletions(-)

(limited to 'interp')

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 9103a5caf0..46be0b8a1f 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -28,24 +28,6 @@ let wit_intro_pattern : (Constrexpr.constr_expr intro_pattern_expr located, glob
 let wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
   Genarg.make0 "tactic"
 
-let wit_tactic0 : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
-  Genarg.make0 "tactic0"
-
-let wit_tactic1 : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
-  Genarg.make0 "tactic1"
-
-let wit_tactic2 : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
-  Genarg.make0 "tactic2"
-
-let wit_tactic3 : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
-  Genarg.make0 "tactic3"
-
-let wit_tactic4 : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
-  Genarg.make0 "tactic4"
-
-let wit_tactic5 : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type =
-  Genarg.make0 "tactic5"
-
 let wit_ltac = Genarg.make0 ~dyn:(val_tag (topwit Stdarg.wit_unit)) "ltac"
 
 let wit_ident =
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index b4029758a3..d38b1183c5 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -71,18 +71,6 @@ val wit_red_expr :
 
 val wit_tactic : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type
 
-val wit_tactic0 : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type
-
-val wit_tactic1 : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type
-
-val wit_tactic2 : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type
-
-val wit_tactic3 : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type
-
-val wit_tactic4 : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type
-
-val wit_tactic5 : (raw_tactic_expr, glob_tactic_expr, Val.t) genarg_type
-
 (** [wit_ltac] is subtly different from [wit_tactic]: they only change for their
     toplevel interpretation. The one of [wit_ltac] forces the tactic and
     discards the result. *)
-- 
cgit v1.2.3