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

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

(limited to 'interp')

diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 46be0b8a1f..9103a5caf0 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -28,6 +28,24 @@ 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 d38b1183c5..b4029758a3 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -71,6 +71,18 @@ 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