3 files changed, 14 insertions, 21 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 6d50c02e2..1a63ca2da 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 67fa0ed7b..d5c48f9e6 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 006885616..11b747e72 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