Removing the use of leveled tactics wit_tacticn. It is now handled

through a unique generic argument, and the level is only considered
at parsing time.

This may introduce unnecessary parentheses in Ltac printing though,
as every tactic argument is collapsed at the lowest level. I assume
this does not matter that much, and anyway Ltac printing is quite
bugged as of today.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16616 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 14 insertions, 21 deletions

diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 6d50c02e24..1a63ca2da1 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -27,7 +27,6 @@ open Tacexpr
 open Genarg
 open Constrarg
 open Mod_subst
-open Extrawit
 open Misctypes
 open Locus
 
@@ -950,9 +949,7 @@ let () =
 
 let () =
   let intern ist tac = (ist, intern_tactic_or_tacarg ist tac) in
-  for i = 0 to 5 do
-    Genintern.register_intern0 (wit_tactic i) intern
-  done
+  Genintern.register_intern0 wit_tactic intern
 
 (***************************************************************************)
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 67fa0ed7b2..d5c48f9e6b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -37,7 +37,6 @@ open Stdarg
 open Constrarg
 open Printer
 open Pretyping
-open Extrawit
 open Evd
 open Misctypes
 open Miscops
@@ -1910,13 +1909,6 @@ and interp_atomic ist gl tac =
         let (sigma,c_interp) = interp_constr_may_eval ist gl (out_gen (glbwit wit_constr_may_eval) x) in
 	evdref := sigma;
 	Value.of_constr c_interp
-    | ExtraArgType s when not (Option.is_empty (tactic_genarg_level s)) ->
-          (* Special treatment of tactic arguments *)
-	let (sigma,v) = val_interp ist gl
-          (out_gen (glbwit (wit_tactic (Option.get (tactic_genarg_level s)))) x)
-	in
-	evdref := sigma;
-	v
     | List0ArgType ConstrArgType ->
         let wit = glbwit (wit_list0 wit_constr) in
 	let (sigma,l_interp) =
@@ -1966,9 +1958,17 @@ and interp_atomic ist gl tac =
     | List0ArgType _ -> app_list0 f x
     | List1ArgType _ -> app_list1 f x
     | ExtraArgType _ ->
-      let (sigma, v) = Geninterp.generic_interp ist { gl with sigma = !evdref } x in
-      evdref := sigma;
-      v
+      (** Special treatment of tactics *)
+      let gl = { gl with sigma = !evdref } in
+      if has_type x (glbwit wit_tactic) then
+        let tac = out_gen (glbwit wit_tactic) x in
+        let (sigma, v) = val_interp ist gl tac in
+        let () = evdref := sigma in
+        v
+      else
+        let (sigma, v) = Geninterp.generic_interp ist gl x in
+        let () = evdref := sigma in
+        v
     | QuantHypArgType | RedExprArgType
     | OpenConstrArgType _ | ConstrWithBindingsArgType
     | BindingsArgType
@@ -2064,9 +2064,7 @@ let () =
     let f = VFun (extract_trace ist, ist.lfun, [], tac) in
     (gl.sigma, TacArg (dloc, valueIn (of_tacvalue f)))
   in
-  for i = 0 to 5 do
-    Geninterp.register_interp0 (wit_tactic i) interp
-  done
+  Geninterp.register_interp0 wit_tactic interp
 
 (***************************************************************************)
 (* Other entry points *)
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 0068856162..11b747e72b 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -329,8 +329,6 @@ and subst_genarg subst (x:glob_generic_argument) =
 let () = Genintern.register_subst0 wit_intro_pattern (fun _ v -> v)
 
 let () =
-  for i = 0 to 5 do
-    Genintern.register_subst0 (Extrawit.wit_tactic i) subst_tactic
-  done
+  Genintern.register_subst0 wit_tactic subst_tactic
 
 let _ = Hook.set Auto.extern_subst_tactic subst_tactic