Uniformizing generic argument types.

Now, instead of having three unrelated types describing a dynamic
type at each level (raw, glob, top), we have a "('a, 'b, 'c) genarg_type"
whose parameters describe the reified type at each level.

This has various advantages:

- No more code duplication to handle the three level separately;
- Safer code: one is not authorized to mix unrelated types when what
was morally expected was a genarg_type.
- Each level-specialized representation can be accessed through
well-typed projections: rawwit, glbwit and topwit.

Documenting a bit Genarg b.t.w.

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

7 files changed, 145 insertions, 141 deletions

diff --git a/tactics/eauto.mli b/tactics/eauto.mli
index 709403a48..00f0cd715 100644
--- a/tactics/eauto.mli
+++ b/tactics/eauto.mli
@@ -16,10 +16,14 @@ open Environ
 open Explore
 
 val hintbases : hint_db_name list option Pcoq.Gram.entry
-val wit_hintbases : hint_db_name list option typed_abstract_argument_type
-val rawwit_hintbases : hint_db_name list option raw_abstract_argument_type
 
-val rawwit_auto_using : Genarg.open_constr_expr list raw_abstract_argument_type
+val wit_hintbases : hint_db_name list option Genarg.uniform_genarg_type
+
+val wit_auto_using :
+  (Genarg.open_constr_expr list,
+  Genarg.open_glob_constr list, Evd.open_constr list)
+    Genarg.genarg_type
+
 
 val e_assumption : tactic
 
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index a15f907c6..21e120a7e 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -283,13 +283,13 @@ let glob_in_arg_hyp_to_clause = gen_in_arg_hyp_to_clause (fun x -> x)
 
 (* spiwack argument for the commands of the retroknowledge *)
 
-let (wit_r_nat_field, globwit_r_nat_field, rawwit_r_nat_field) =
+let wit_r_nat_field =
   Genarg.create_arg None "r_nat_field"
-let (wit_r_n_field, globwit_r_n_field, rawwit_r_n_field) =
+let wit_r_n_field =
   Genarg.create_arg None "r_n_field"
-let (wit_r_int31_field, globwit_r_int31_field, rawwit_r_int31_field) =
+let wit_r_int31_field =
   Genarg.create_arg None "r_int31_field"
-let (wit_r_field, globwit_r_field, rawwit_r_field) =
+let wit_r_field =
   Genarg.create_arg None "r_field"
 
 (* spiwack: the print functions are incomplete, but I don't know what they are
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 7fc3ac8a5..cd4d777d6 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -15,20 +15,19 @@ open Termops
 open Glob_term
 open Misctypes
 
-val rawwit_orient : bool raw_abstract_argument_type
-val globwit_orient : bool glob_abstract_argument_type
-val wit_orient : bool typed_abstract_argument_type
+val wit_orient : bool Genarg.uniform_genarg_type
 val orient : bool Pcoq.Gram.entry
 val pr_orient : bool -> Pp.std_ppcmds
 
 val occurrences : (int list or_var) Pcoq.Gram.entry
-val rawwit_occurrences : (int list or_var) raw_abstract_argument_type
-val wit_occurrences : (int list) typed_abstract_argument_type
+val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg_type
 val pr_occurrences : int list or_var -> Pp.std_ppcmds
 val occurrences_of : int list -> Locus.occurrences
 
-val rawwit_glob : constr_expr raw_abstract_argument_type
-val wit_glob : (Tacinterp.interp_sign * glob_constr) typed_abstract_argument_type
+val wit_glob :
+  (constr_expr,
+  Genarg.glob_constr_and_expr,
+  Tacinterp.interp_sign * glob_constr) Genarg.genarg_type
 val glob : constr_expr Pcoq.Gram.entry
 
 type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location
@@ -36,22 +35,27 @@ type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location
 type loc_place = Id.t Loc.located gen_place
 type place = Id.t gen_place
 
-val rawwit_hloc : loc_place raw_abstract_argument_type
-val wit_hloc : place typed_abstract_argument_type
+val wit_hloc : (loc_place, loc_place, place) Genarg.genarg_type
 val hloc : loc_place Pcoq.Gram.entry
 val pr_hloc : loc_place -> Pp.std_ppcmds
 
 val in_arg_hyp:  (Names.Id.t Loc.located list option * bool)  Pcoq.Gram.entry
-val globwit_in_arg_hyp : (Names.Id.t Loc.located list option * bool) glob_abstract_argument_type
-val rawwit_in_arg_hyp : (Names.Id.t Loc.located list option * bool) raw_abstract_argument_type
-val wit_in_arg_hyp : (Names.Id.t list option * bool) typed_abstract_argument_type
+
+val wit_in_arg_hyp :
+  ((Names.Id.t Loc.located list option * bool),
+  (Names.Id.t Loc.located list option * bool),
+  (Names.Id.t list option * bool)) Genarg.genarg_type
+
 val raw_in_arg_hyp_to_clause : (Names.Id.t Loc.located list option * bool) -> Locus.clause
 val glob_in_arg_hyp_to_clause :  (Names.Id.t list option * bool)  -> Locus.clause
 val pr_in_arg_hyp : (Names.Id.t list option * bool) -> Pp.std_ppcmds
 
 val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry
-val rawwit_by_arg_tac :  raw_tactic_expr option raw_abstract_argument_type
-val wit_by_arg_tac : glob_tactic_expr option typed_abstract_argument_type
+val wit_by_arg_tac :
+  (raw_tactic_expr option,
+  glob_tactic_expr option,
+  glob_tactic_expr option) Genarg.genarg_type
+
 val pr_by_arg_tac : 
   (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) ->
   raw_tactic_expr option -> Pp.std_ppcmds
@@ -60,5 +64,4 @@ val pr_by_arg_tac :
 (** Spiwack: Primitive for retroknowledge registration *)
 
 val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
-val rawwit_retroknowledge_field :  Retroknowledge.field raw_abstract_argument_type
-val wit_retroknowledge_field : Retroknowledge.field typed_abstract_argument_type
+val wit_retroknowledge_field : Retroknowledge.field Genarg.uniform_genarg_type
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index f7c13d01a..0e8b5a2db 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1665,13 +1665,10 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 	     (Ident (Loc.ghost,Id.of_string "Equivalence_Symmetric"), lemma2);
 	     (Ident (Loc.ghost,Id.of_string "Equivalence_Transitive"), lemma3)])
 
-type 'a binders_argtype = (local_binder list, 'a) Genarg.abstract_argument_type
+type binders_argtype = local_binder list
 
-let _, _, rawwit_binders =
- (Genarg.create_arg None "binders" :
-    Genarg.tlevel binders_argtype *
-    Genarg.glevel binders_argtype *
-    Genarg.rlevel binders_argtype)
+let wit_binders =
+ (Genarg.create_arg None "binders" : binders_argtype Genarg.uniform_genarg_type)
 
 open Pcoq.Constr
 
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 4662494aa..aa91db9b0 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -765,49 +765,49 @@ and intern_match_rule onlytac ist = function
 
 and intern_genarg ist x =
   match genarg_tag x with
-  | BoolArgType -> in_gen globwit_bool (out_gen rawwit_bool x)
-  | IntArgType -> in_gen globwit_int (out_gen rawwit_int x)
+  | BoolArgType -> in_gen (glbwit wit_bool) (out_gen (rawwit wit_bool) x)
+  | IntArgType -> in_gen (glbwit wit_int) (out_gen (rawwit wit_int) x)
   | IntOrVarArgType ->
-      in_gen globwit_int_or_var
-        (intern_or_var ist (out_gen rawwit_int_or_var x))
+      in_gen (glbwit wit_int_or_var)
+        (intern_or_var ist (out_gen (rawwit wit_int_or_var) x))
   | StringArgType ->
-      in_gen globwit_string (out_gen rawwit_string x)
+      in_gen (glbwit wit_string) (out_gen (rawwit wit_string) x)
   | PreIdentArgType ->
-      in_gen globwit_pre_ident (out_gen rawwit_pre_ident x)
+      in_gen (glbwit wit_pre_ident) (out_gen (rawwit wit_pre_ident) x)
   | IntroPatternArgType ->
       let lf = ref ([],[]) in
       (* how to know which names are bound by the intropattern *)
-      in_gen globwit_intro_pattern
-        (intern_intro_pattern lf ist (out_gen rawwit_intro_pattern x))
+      in_gen (glbwit wit_intro_pattern)
+        (intern_intro_pattern lf ist (out_gen (rawwit wit_intro_pattern) x))
   | IdentArgType b ->
       let lf = ref ([],[]) in
-      in_gen (globwit_ident_gen b)
-	(intern_ident lf ist (out_gen (rawwit_ident_gen b) x))
+      in_gen (glbwit (wit_ident_gen b))
+	(intern_ident lf ist (out_gen (rawwit (wit_ident_gen b)) x))
   | VarArgType ->
-      in_gen globwit_var (intern_hyp ist (out_gen rawwit_var x))
+      in_gen (glbwit wit_var) (intern_hyp ist (out_gen (rawwit wit_var) x))
   | RefArgType ->
-      in_gen globwit_ref (intern_global_reference ist (out_gen rawwit_ref x))
+      in_gen (glbwit wit_ref) (intern_global_reference ist (out_gen (rawwit wit_ref) x))
   | SortArgType ->
-      in_gen globwit_sort (out_gen rawwit_sort x)
+      in_gen (glbwit wit_sort) (out_gen (rawwit wit_sort) x)
   | ConstrArgType ->
-      in_gen globwit_constr (intern_constr ist (out_gen rawwit_constr x))
+      in_gen (glbwit wit_constr) (intern_constr ist (out_gen (rawwit wit_constr) x))
   | ConstrMayEvalArgType ->
-      in_gen globwit_constr_may_eval
-        (intern_constr_may_eval ist (out_gen rawwit_constr_may_eval x))
+      in_gen (glbwit wit_constr_may_eval)
+        (intern_constr_may_eval ist (out_gen (rawwit wit_constr_may_eval) x))
   | QuantHypArgType ->
-      in_gen globwit_quant_hyp
-        (intern_quantified_hypothesis ist (out_gen rawwit_quant_hyp x))
+      in_gen (glbwit wit_quant_hyp)
+        (intern_quantified_hypothesis ist (out_gen (rawwit wit_quant_hyp) x))
   | RedExprArgType ->
-      in_gen globwit_red_expr (intern_red_expr ist (out_gen rawwit_red_expr x))
+      in_gen (glbwit wit_red_expr) (intern_red_expr ist (out_gen (rawwit wit_red_expr) x))
   | OpenConstrArgType b ->
-      in_gen (globwit_open_constr_gen b)
-        ((),intern_constr ist (snd (out_gen (rawwit_open_constr_gen b) x)))
+      in_gen (glbwit (wit_open_constr_gen b))
+        ((),intern_constr ist (snd (out_gen (rawwit (wit_open_constr_gen b)) x)))
   | ConstrWithBindingsArgType ->
-      in_gen globwit_constr_with_bindings
-        (intern_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x))
+      in_gen (glbwit wit_constr_with_bindings)
+        (intern_constr_with_bindings ist (out_gen (rawwit wit_constr_with_bindings) x))
   | BindingsArgType ->
-      in_gen globwit_bindings
-        (intern_bindings ist (out_gen rawwit_bindings x))
+      in_gen (glbwit wit_bindings)
+        (intern_bindings ist (out_gen (rawwit wit_bindings) x))
   | List0ArgType _ -> app_list0 (intern_genarg ist) x
   | List1ArgType _ -> app_list1 (intern_genarg ist) x
   | OptArgType _ -> app_opt (intern_genarg ist) x
@@ -816,8 +816,8 @@ and intern_genarg ist x =
       match tactic_genarg_level s with
       | Some n ->
           (* Special treatment of tactic arguments *)
-          in_gen (globwit_tactic n) (intern_tactic_or_tacarg ist
-	    (out_gen (rawwit_tactic n) x))
+          in_gen (glbwit (wit_tactic n)) (intern_tactic_or_tacarg ist
+	    (out_gen (rawwit (wit_tactic n)) x))
       | None ->
           lookup_intern_genarg s ist x
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index c0903c2a9..1458cd73b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1371,63 +1371,63 @@ and interp_genarg ist gl x =
   let rec interp_genarg ist gl x =
     let gl = { gl with sigma = !evdref } in
     match genarg_tag x with
-    | BoolArgType -> in_gen wit_bool (out_gen globwit_bool x)
-    | IntArgType -> in_gen wit_int (out_gen globwit_int x)
+    | BoolArgType -> in_gen (topwit wit_bool) (out_gen (glbwit wit_bool) x)
+    | IntArgType -> in_gen (topwit wit_int) (out_gen (glbwit wit_int) x)
     | IntOrVarArgType ->
-      in_gen wit_int_or_var
-        (ArgArg (interp_int_or_var ist (out_gen globwit_int_or_var x)))
+      in_gen (topwit wit_int_or_var)
+        (ArgArg (interp_int_or_var ist (out_gen (glbwit wit_int_or_var) x)))
     | StringArgType ->
-      in_gen wit_string (out_gen globwit_string x)
+      in_gen (topwit wit_string) (out_gen (glbwit wit_string) x)
     | PreIdentArgType ->
-      in_gen wit_pre_ident (out_gen globwit_pre_ident x)
+      in_gen (topwit wit_pre_ident) (out_gen (glbwit wit_pre_ident) x)
     | IntroPatternArgType ->
-      in_gen wit_intro_pattern
-        (interp_intro_pattern ist gl (out_gen globwit_intro_pattern x))
+      in_gen (topwit wit_intro_pattern)
+        (interp_intro_pattern ist gl (out_gen (glbwit wit_intro_pattern) x))
     | IdentArgType b ->
-      in_gen (wit_ident_gen b)
-        (pf_interp_fresh_ident ist gl (out_gen (globwit_ident_gen b) x))
+      in_gen (topwit (wit_ident_gen b))
+        (pf_interp_fresh_ident ist gl (out_gen (glbwit (wit_ident_gen b)) x))
     | VarArgType ->
-      in_gen wit_var (interp_hyp ist gl (out_gen globwit_var x))
+      in_gen (topwit wit_var) (interp_hyp ist gl (out_gen (glbwit wit_var) x))
     | RefArgType ->
-      in_gen wit_ref (pf_interp_reference ist gl (out_gen globwit_ref x))
+      in_gen (topwit wit_ref) (pf_interp_reference ist gl (out_gen (glbwit wit_ref) x))
     | SortArgType ->
       let (sigma,c_interp) =
 	pf_interp_constr ist gl
-	  (GSort (dloc,out_gen globwit_sort x), None)
+	  (GSort (dloc,out_gen (glbwit wit_sort) x), None)
       in
       evdref := sigma;
-      in_gen wit_sort
+      in_gen (topwit wit_sort)
         (destSort c_interp)
     | ConstrArgType ->
-      let (sigma,c_interp) = pf_interp_constr ist gl (out_gen globwit_constr x) in
+      let (sigma,c_interp) = pf_interp_constr ist gl (out_gen (glbwit wit_constr) x) in
       evdref := sigma;
-      in_gen wit_constr c_interp
+      in_gen (topwit wit_constr) c_interp
     | ConstrMayEvalArgType ->
-      let (sigma,c_interp) = interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x) in
+      let (sigma,c_interp) = interp_constr_may_eval ist gl (out_gen (glbwit wit_constr_may_eval) x) in
       evdref := sigma;
-      in_gen wit_constr_may_eval c_interp
+      in_gen (topwit wit_constr_may_eval) c_interp
     | QuantHypArgType ->
-      in_gen wit_quant_hyp
+      in_gen (topwit wit_quant_hyp)
         (interp_declared_or_quantified_hypothesis ist gl
-           (out_gen globwit_quant_hyp x))
+           (out_gen (glbwit wit_quant_hyp) x))
     | RedExprArgType ->
-      let (sigma,r_interp) = pf_interp_red_expr ist gl (out_gen globwit_red_expr x) in
+      let (sigma,r_interp) = pf_interp_red_expr ist gl (out_gen (glbwit wit_red_expr) x) in
       evdref := sigma;
-      in_gen wit_red_expr r_interp
+      in_gen (topwit wit_red_expr) r_interp
     | OpenConstrArgType casted ->
       let expected_type =
         if casted then OfType (pf_concl gl) else WithoutTypeConstraint in
-      in_gen (wit_open_constr_gen casted)
+      in_gen (topwit (wit_open_constr_gen casted))
         (interp_open_constr ~expected_type
            ist (pf_env gl) (project gl)
-           (snd (out_gen (globwit_open_constr_gen casted) x)))
+           (snd (out_gen (glbwit (wit_open_constr_gen casted)) x)))
     | ConstrWithBindingsArgType ->
-      in_gen wit_constr_with_bindings
+      in_gen (topwit wit_constr_with_bindings)
         (pack_sigma (interp_constr_with_bindings ist (pf_env gl) (project gl)
-		       (out_gen globwit_constr_with_bindings x)))
+		       (out_gen (glbwit wit_constr_with_bindings) x)))
     | BindingsArgType ->
-      in_gen wit_bindings
-        (pack_sigma (interp_bindings ist (pf_env gl) (project gl) (out_gen globwit_bindings x)))
+      in_gen (topwit wit_bindings)
+        (pack_sigma (interp_bindings ist (pf_env gl) (project gl) (out_gen (glbwit wit_bindings) x)))
     | List0ArgType ConstrArgType ->
         let (sigma,v) = interp_genarg_constr_list0 ist gl x in
 	evdref := sigma;
@@ -1446,9 +1446,9 @@ and interp_genarg ist gl x =
       match tactic_genarg_level s with
       | Some n ->
           (* Special treatment of tactic arguments *)
-        in_gen (wit_tactic n)
+        in_gen (topwit (wit_tactic n))
 	  (TacArg(dloc,valueIn(VFun(ist.trace,ist.lfun,[],
-				    out_gen (globwit_tactic n) x))))
+				    out_gen (glbwit (wit_tactic n)) x))))
       | None ->
         let (sigma,v) = lookup_interp_genarg s ist gl x in
 	evdref:=sigma;
@@ -1458,24 +1458,24 @@ and interp_genarg ist gl x =
   !evdref , v
 
 and interp_genarg_constr_list0 ist gl x =
-  let lc = out_gen (wit_list0 globwit_constr) x in
+  let lc = out_gen (glbwit (wit_list0 wit_constr)) x in
   let (sigma,lc) = pf_apply (interp_constr_list ist) gl lc in
-  sigma , in_gen (wit_list0 wit_constr) lc
+  sigma , in_gen (topwit (wit_list0 wit_constr)) lc
 
 and interp_genarg_constr_list1 ist gl x =
-  let lc = out_gen (wit_list1 globwit_constr) x in
+  let lc = out_gen (glbwit (wit_list1 wit_constr)) x in
   let (sigma,lc) = pf_apply (interp_constr_list ist) gl lc in
-  sigma , in_gen (wit_list1 wit_constr) lc
+  sigma , in_gen (topwit (wit_list1 wit_constr)) lc
 
 and interp_genarg_var_list0 ist gl x =
-  let lc = out_gen (wit_list0 globwit_var) x in
+  let lc = out_gen (glbwit (wit_list0 wit_var)) x in
   let lc = interp_hyp_list ist gl lc in
-  in_gen (wit_list0 wit_var) lc
+  in_gen (topwit (wit_list0 wit_var)) lc
 
 and interp_genarg_var_list1 ist gl x =
-  let lc = out_gen (wit_list1 globwit_var) x in
+  let lc = out_gen (glbwit (wit_list1 wit_var)) x in
   let lc = interp_hyp_list ist gl lc in
-  in_gen (wit_list1 wit_var) lc
+  in_gen (topwit (wit_list1 wit_var)) lc
 
 (* Interprets the Match expressions *)
 and interp_match ist g lz constr lmr =
@@ -1885,45 +1885,45 @@ and interp_atomic ist gl tac =
     let evdref = ref gl.sigma in
     let f x = match genarg_tag x with
     | IntArgType ->
-        VInteger (out_gen globwit_int x)
+        VInteger (out_gen (glbwit wit_int) x)
     | IntOrVarArgType ->
-        mk_int_or_var_value ist (out_gen globwit_int_or_var x)
+        mk_int_or_var_value ist (out_gen (glbwit wit_int_or_var) x)
     | PreIdentArgType ->
 	failwith "pre-identifiers cannot be bound"
     | IntroPatternArgType ->
 	VIntroPattern
-	  (snd (interp_intro_pattern ist gl (out_gen globwit_intro_pattern x)))
+	  (snd (interp_intro_pattern ist gl (out_gen (glbwit wit_intro_pattern) x)))
     | IdentArgType b ->
 	value_of_ident (interp_fresh_ident ist env
-	  (out_gen (globwit_ident_gen b) x))
+	  (out_gen (glbwit (wit_ident_gen b)) x))
     | VarArgType ->
-        mk_hyp_value ist gl (out_gen globwit_var x)
+        mk_hyp_value ist gl (out_gen (glbwit wit_var) x)
     | RefArgType ->
         VConstr ([],constr_of_global
-          (pf_interp_reference ist gl (out_gen globwit_ref x)))
+          (pf_interp_reference ist gl (out_gen (glbwit wit_ref) x)))
     | SortArgType ->
-        VConstr ([],mkSort (interp_sort (out_gen globwit_sort x)))
+        VConstr ([],mkSort (interp_sort (out_gen (glbwit wit_sort) x)))
     | ConstrArgType ->
-        let (sigma,v) = mk_constr_value ist gl (out_gen globwit_constr x) in
+        let (sigma,v) = mk_constr_value ist gl (out_gen (glbwit wit_constr) x) in
 	evdref := sigma;
 	v
     | OpenConstrArgType false ->
-        let (sigma,v) = mk_open_constr_value ist gl (snd (out_gen globwit_open_constr x)) in
+        let (sigma,v) = mk_open_constr_value ist gl (snd (out_gen (glbwit wit_open_constr) x)) in
 	evdref := sigma;
 	v
     | ConstrMayEvalArgType ->
-        let (sigma,c_interp) = interp_constr_may_eval ist gl (out_gen globwit_constr_may_eval x) in
+        let (sigma,c_interp) = interp_constr_may_eval ist gl (out_gen (glbwit wit_constr_may_eval) x) in
 	evdref := sigma;
 	VConstr ([],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 (globwit_tactic (Option.get (tactic_genarg_level s))) x)
+          (out_gen (glbwit (wit_tactic (Option.get (tactic_genarg_level s)))) x)
 	in
 	evdref := sigma;
 	v
     | List0ArgType ConstrArgType ->
-        let wit = wit_list0 globwit_constr in
+        let wit = glbwit (wit_list0 wit_constr) in
 	let (sigma,l_interp) =
 	  List.fold_right begin fun c (sigma,acc) ->
 	    let (sigma,c_interp) = mk_constr_value ist { gl with sigma=sigma } c in
@@ -1933,24 +1933,24 @@ and interp_atomic ist gl tac =
 	evdref := sigma;
         VList (l_interp)
     | List0ArgType VarArgType ->
-        let wit = wit_list0 globwit_var in
+        let wit = glbwit (wit_list0 wit_var) in
         VList (List.map (mk_hyp_value ist gl) (out_gen wit x))
     | List0ArgType IntArgType ->
-        let wit = wit_list0 globwit_int in
+        let wit = glbwit (wit_list0 wit_int) in
         VList (List.map (fun x -> VInteger x) (out_gen wit x))
     | List0ArgType IntOrVarArgType ->
-        let wit = wit_list0 globwit_int_or_var in
+        let wit = glbwit (wit_list0 wit_int_or_var) in
         VList (List.map (mk_int_or_var_value ist) (out_gen wit x))
     | List0ArgType (IdentArgType b) ->
-        let wit = wit_list0 (globwit_ident_gen b) in
+        let wit = glbwit (wit_list0 (wit_ident_gen b)) in
 	let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in
         VList (List.map mk_ident (out_gen wit x))
     | List0ArgType IntroPatternArgType ->
-        let wit = wit_list0 globwit_intro_pattern in
+        let wit = glbwit (wit_list0 wit_intro_pattern) in
 	let mk_ipat x = VIntroPattern (snd (interp_intro_pattern ist gl x)) in
         VList (List.map mk_ipat (out_gen wit x))
     | List1ArgType ConstrArgType ->
-        let wit = wit_list1 globwit_constr in
+        let wit = glbwit (wit_list1 wit_constr) in
 	let (sigma, l_interp) =
 	  List.fold_right begin fun c (sigma,acc) ->
 	    let (sigma,c_interp) = mk_constr_value ist { gl with sigma=sigma } c in
@@ -1960,20 +1960,20 @@ and interp_atomic ist gl tac =
 	evdref:=sigma;
         VList l_interp
     | List1ArgType VarArgType ->
-        let wit = wit_list1 globwit_var in
+        let wit = glbwit (wit_list1 wit_var) in
         VList (List.map (mk_hyp_value ist gl) (out_gen wit x))
     | List1ArgType IntArgType ->
-        let wit = wit_list1 globwit_int in
+        let wit = glbwit (wit_list1 wit_int) in
         VList (List.map (fun x -> VInteger x) (out_gen wit x))
     | List1ArgType IntOrVarArgType ->
-        let wit = wit_list1 globwit_int_or_var in
+        let wit = glbwit (wit_list1 wit_int_or_var) in
         VList (List.map (mk_int_or_var_value ist) (out_gen wit x))
     | List1ArgType (IdentArgType b) ->
-        let wit = wit_list1 (globwit_ident_gen b) in
+        let wit = glbwit (wit_list1 (wit_ident_gen b)) in
 	let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in
         VList (List.map mk_ident (out_gen wit x))
     | List1ArgType IntroPatternArgType ->
-        let wit = wit_list1 globwit_intro_pattern in
+        let wit = glbwit (wit_list1 wit_intro_pattern) in
 	let mk_ipat x = VIntroPattern (snd (interp_intro_pattern ist gl x)) in
         VList (List.map mk_ipat (out_gen wit x))
     | StringArgType | BoolArgType
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 1cf4264ea..bb7caf93b 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -300,40 +300,40 @@ and subst_match_rule subst = function
 
 and subst_genarg subst (x:glob_generic_argument) =
   match genarg_tag x with
-  | BoolArgType -> in_gen globwit_bool (out_gen globwit_bool x)
-  | IntArgType -> in_gen globwit_int (out_gen globwit_int x)
-  | IntOrVarArgType -> in_gen globwit_int_or_var (out_gen globwit_int_or_var x)
-  | StringArgType -> in_gen globwit_string (out_gen globwit_string x)
-  | PreIdentArgType -> in_gen globwit_pre_ident (out_gen globwit_pre_ident x)
+  | BoolArgType -> in_gen (glbwit wit_bool) (out_gen (glbwit wit_bool) x)
+  | IntArgType -> in_gen (glbwit wit_int) (out_gen (glbwit wit_int) x)
+  | IntOrVarArgType -> in_gen (glbwit wit_int_or_var) (out_gen (glbwit wit_int_or_var) x)
+  | StringArgType -> in_gen (glbwit wit_string) (out_gen (glbwit wit_string) x)
+  | PreIdentArgType -> in_gen (glbwit wit_pre_ident) (out_gen (glbwit wit_pre_ident) x)
   | IntroPatternArgType ->
-      in_gen globwit_intro_pattern (out_gen globwit_intro_pattern x)
+      in_gen (glbwit wit_intro_pattern) (out_gen (glbwit wit_intro_pattern) x)
   | IdentArgType b ->
-      in_gen (globwit_ident_gen b) (out_gen (globwit_ident_gen b) x)
-  | VarArgType -> in_gen globwit_var (out_gen globwit_var x)
+      in_gen (glbwit (wit_ident_gen b)) (out_gen (glbwit (wit_ident_gen b)) x)
+  | VarArgType -> in_gen (glbwit wit_var) (out_gen (glbwit wit_var) x)
   | RefArgType ->
-      in_gen globwit_ref (subst_global_reference subst
-	(out_gen globwit_ref x))
+      in_gen (glbwit wit_ref) (subst_global_reference subst
+	(out_gen (glbwit wit_ref) x))
   | SortArgType ->
-      in_gen globwit_sort (out_gen globwit_sort x)
+      in_gen (glbwit wit_sort) (out_gen (glbwit wit_sort) x)
   | ConstrArgType ->
-      in_gen globwit_constr (subst_glob_constr subst (out_gen globwit_constr x))
+      in_gen (glbwit wit_constr) (subst_glob_constr subst (out_gen (glbwit wit_constr) x))
   | ConstrMayEvalArgType ->
-      in_gen globwit_constr_may_eval (subst_raw_may_eval subst (out_gen globwit_constr_may_eval x))
+      in_gen (glbwit wit_constr_may_eval) (subst_raw_may_eval subst (out_gen (glbwit wit_constr_may_eval) x))
   | QuantHypArgType ->
-      in_gen globwit_quant_hyp
+      in_gen (glbwit wit_quant_hyp)
         (subst_declared_or_quantified_hypothesis subst
-          (out_gen globwit_quant_hyp x))
+          (out_gen (glbwit wit_quant_hyp) x))
   | RedExprArgType ->
-      in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x))
+      in_gen (glbwit wit_red_expr) (subst_redexp subst (out_gen (glbwit wit_red_expr) x))
   | OpenConstrArgType b ->
-      in_gen (globwit_open_constr_gen b)
-        ((),subst_glob_constr subst (snd (out_gen (globwit_open_constr_gen b) x)))
+      in_gen (glbwit (wit_open_constr_gen b))
+        ((),subst_glob_constr subst (snd (out_gen (glbwit (wit_open_constr_gen b)) x)))
   | ConstrWithBindingsArgType ->
-      in_gen globwit_constr_with_bindings
-        (subst_glob_with_bindings subst (out_gen globwit_constr_with_bindings x))
+      in_gen (glbwit wit_constr_with_bindings)
+        (subst_glob_with_bindings subst (out_gen (glbwit wit_constr_with_bindings) x))
   | BindingsArgType ->
-      in_gen globwit_bindings
-        (subst_bindings subst (out_gen globwit_bindings x))
+      in_gen (glbwit wit_bindings)
+        (subst_bindings subst (out_gen (glbwit wit_bindings) x))
   | List0ArgType _ -> app_list0 (subst_genarg subst) x
   | List1ArgType _ -> app_list1 (subst_genarg subst) x
   | OptArgType _ -> app_opt (subst_genarg subst) x
@@ -342,8 +342,8 @@ and subst_genarg subst (x:glob_generic_argument) =
       match Extrawit.tactic_genarg_level s with
       | Some n ->
           (* Special treatment of tactic arguments *)
-          in_gen (Extrawit.globwit_tactic n)
-            (subst_tactic subst (out_gen (Extrawit.globwit_tactic n) x))
+          in_gen (glbwit (Extrawit.wit_tactic n))
+            (subst_tactic subst (out_gen (glbwit (Extrawit.wit_tactic n)) x))
       | None ->
           lookup_genarg_subst s subst x