Suppression du type 'tac dans les abstract_argument_type: devenu inutile

suite à l'adoption du modèle rlevel,glevel,tlevel et au passage des 
wit_tactic en types créés dynamiquement (révisions 8917 et 8926).


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

7 files changed, 166 insertions, 162 deletions

diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 3d9c763815..4ed0b018cf 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -69,11 +69,11 @@ GEXTEND Gram
   END
 
 
-type ('a,'b) gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a, 'b) Genarg.abstract_argument_type
+type 'a gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a) Genarg.abstract_argument_type
 
-let (wit_subtac_gallina_loc : (Genarg.tlevel, Proof_type.tactic) gallina_loc_argtype),
-  (globwit_subtac_gallina_loc : (Genarg.glevel, Tacexpr.glob_tactic_expr) gallina_loc_argtype),
-  (rawwit_subtac_gallina_loc : (Genarg.rlevel, Tacexpr.raw_tactic_expr) gallina_loc_argtype) =
+let (wit_subtac_gallina_loc : Genarg.tlevel gallina_loc_argtype),
+  (globwit_subtac_gallina_loc : Genarg.glevel gallina_loc_argtype),
+  (rawwit_subtac_gallina_loc : Genarg.rlevel gallina_loc_argtype) =
   Genarg.create_arg "subtac_gallina_loc"
 
 VERNAC COMMAND EXTEND Subtac
diff --git a/interp/genarg.ml b/interp/genarg.ml
index e5713a6e28..303278f18d 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -48,7 +48,7 @@ type rawconstr_and_expr = rawconstr * constr_expr option
 
 (* Dynamics but tagged by a type expression *)
 
-type ('a,'b) generic_argument = argument_type * Obj.t
+type 'a generic_argument = argument_type * Obj.t
 
 let dyntab = ref ([] : string list)
 
@@ -56,7 +56,7 @@ type rlevel = constr_expr
 type glevel = rawconstr_and_expr
 type tlevel = constr
 
-type ('a,'b,'c) abstract_argument_type = argument_type
+type ('a,'b) abstract_argument_type = argument_type
 
 let create_arg s =
   if List.mem s !dyntab then
diff --git a/interp/genarg.mli b/interp/genarg.mli
index d2aa750cc5..3530bd27ce 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -40,21 +40,34 @@ val pr_case_intro_pattern : case_intro_pattern_expr -> Pp.std_ppcmds
 (* The route of a generic argument, from parsing to evaluation
 
 \begin{verbatim}
-              parsing        in_raw                           out_raw
-    char stream ----> rawtype ----> rawconstr generic_argument ---->
-                                                                   |
-                                                                   | interp
-                                                                   V
-                          type  <---- constr generic_argument  <----
-                                  out                            in
+             parsing        in_raw                              out_raw
+   char stream ----> rawtype ----> constr_expr generic_argument --------|
+                          encapsulation                         decaps  |
+                                                                        |
+                                                                        V
+                                                                     rawtype
+                                                                        |
+                                                         globalization  |
+                                                                        V
+                                                                    glob_type
+                                                                        |
+                                                                 encaps |
+                                                                in_glob |
+                                                                        V
+                                                     rawconstr generic_argument
+                                                                        |
+        out                          in                        out_glob |
+  type <--- constr generic_argument <---- type <------ rawtype <--------|
+    |  decaps                       encaps      interp           decaps
+    |
+    V
+effective use
 \end{verbatim}
 
-To distinguish between the uninterpreted (raw) and the interpreted
-worlds, we annotate the type [generic_argument] by a phantom argument
-which is either [constr_expr] or [constr] (actually we add also a second
-argument [raw_tactic_expr] and [tactic], but this is only for technical
-reasons, because these types are undefined at the type of compilation
-of [Genarg]).
+To distinguish between the uninterpreted (raw), globalized and 
+interpreted worlds, we annotate the type [generic_argument] by a
+phantom argument which is either [constr_expr], [rawconstr] or
+[constr].
 
 Transformation for each type :
 \begin{verbatim}
@@ -84,8 +97,8 @@ ExtraArgType of string         '_a                      '_b
 
 (* All of [rlevel], [glevel] and [tlevel] must be non convertible 
    to ensure the injectivity of the type inference from type
-   [('co,'ta) generic_argument] to [('a,'co,'ta) abstract_argument_type]
-   is injective; this guarantees that, for 'b fixed, the type of
+   ['co generic_argument] to [('a,'co) abstract_argument_type];
+   this guarantees that, for 'co fixed, the type of
    out_gen is monomorphic over 'a, hence type-safe 
 *)
 
@@ -93,138 +106,137 @@ type rlevel = constr_expr
 type glevel = rawconstr_and_expr
 type tlevel = constr
 
-type ('a,'co,'ta) abstract_argument_type
+type ('a,'co) abstract_argument_type
 
-val rawwit_bool : (bool,rlevel,'ta) abstract_argument_type
-val globwit_bool : (bool,glevel,'ta) abstract_argument_type
-val wit_bool : (bool,tlevel,'ta) abstract_argument_type
+val rawwit_bool : (bool,rlevel) abstract_argument_type
+val globwit_bool : (bool,glevel) abstract_argument_type
+val wit_bool : (bool,tlevel) abstract_argument_type
 
-val rawwit_int : (int,rlevel,'ta) abstract_argument_type
-val globwit_int : (int,glevel,'ta) abstract_argument_type
-val wit_int : (int,tlevel,'ta) abstract_argument_type
+val rawwit_int : (int,rlevel) abstract_argument_type
+val globwit_int : (int,glevel) abstract_argument_type
+val wit_int : (int,tlevel) abstract_argument_type
 
-val rawwit_int_or_var : (int or_var,rlevel,'ta) abstract_argument_type
-val globwit_int_or_var : (int or_var,glevel,'ta) abstract_argument_type
-val wit_int_or_var : (int or_var,tlevel,'ta) abstract_argument_type
+val rawwit_int_or_var : (int or_var,rlevel) abstract_argument_type
+val globwit_int_or_var : (int or_var,glevel) abstract_argument_type
+val wit_int_or_var : (int or_var,tlevel) abstract_argument_type
 
-val rawwit_string : (string,rlevel,'ta) abstract_argument_type
-val globwit_string : (string,glevel,'ta) abstract_argument_type
-val wit_string : (string,tlevel,'ta) abstract_argument_type
+val rawwit_string : (string,rlevel) abstract_argument_type
+val globwit_string : (string,glevel) abstract_argument_type
+val wit_string : (string,tlevel) abstract_argument_type
 
-val rawwit_pre_ident : (string,rlevel,'ta) abstract_argument_type
-val globwit_pre_ident : (string,glevel,'ta) abstract_argument_type
-val wit_pre_ident : (string,tlevel,'ta) abstract_argument_type
+val rawwit_pre_ident : (string,rlevel) abstract_argument_type
+val globwit_pre_ident : (string,glevel) abstract_argument_type
+val wit_pre_ident : (string,tlevel) abstract_argument_type
 
-val rawwit_intro_pattern : (intro_pattern_expr,rlevel,'ta) abstract_argument_type
-val globwit_intro_pattern : (intro_pattern_expr,glevel,'ta) abstract_argument_type
-val wit_intro_pattern : (intro_pattern_expr,tlevel,'ta) abstract_argument_type
+val rawwit_intro_pattern : (intro_pattern_expr,rlevel) abstract_argument_type
+val globwit_intro_pattern : (intro_pattern_expr,glevel) abstract_argument_type
+val wit_intro_pattern : (intro_pattern_expr,tlevel) abstract_argument_type
 
-val rawwit_ident : (identifier,rlevel,'ta) abstract_argument_type
-val globwit_ident : (identifier,glevel,'ta) abstract_argument_type
-val wit_ident : (identifier,tlevel,'ta) abstract_argument_type
+val rawwit_ident : (identifier,rlevel) abstract_argument_type
+val globwit_ident : (identifier,glevel) abstract_argument_type
+val wit_ident : (identifier,tlevel) abstract_argument_type
 
-val rawwit_var : (identifier located,rlevel,'ta) abstract_argument_type
-val globwit_var : (identifier located,glevel,'ta) abstract_argument_type
-val wit_var : (identifier,tlevel,'ta) abstract_argument_type
+val rawwit_var : (identifier located,rlevel) abstract_argument_type
+val globwit_var : (identifier located,glevel) abstract_argument_type
+val wit_var : (identifier,tlevel) abstract_argument_type
 
-val rawwit_ref : (reference,rlevel,'ta) abstract_argument_type
-val globwit_ref : (global_reference located or_var,glevel,'ta) abstract_argument_type
-val wit_ref : (global_reference,tlevel,'ta) abstract_argument_type
+val rawwit_ref : (reference,rlevel) abstract_argument_type
+val globwit_ref : (global_reference located or_var,glevel) abstract_argument_type
+val wit_ref : (global_reference,tlevel) abstract_argument_type
 
-val rawwit_quant_hyp : (quantified_hypothesis,rlevel,'ta) abstract_argument_type
-val globwit_quant_hyp : (quantified_hypothesis,glevel,'ta) abstract_argument_type
-val wit_quant_hyp : (quantified_hypothesis,tlevel,'ta) abstract_argument_type
+val rawwit_quant_hyp : (quantified_hypothesis,rlevel) abstract_argument_type
+val globwit_quant_hyp : (quantified_hypothesis,glevel) abstract_argument_type
+val wit_quant_hyp : (quantified_hypothesis,tlevel) abstract_argument_type
 
-val rawwit_sort : (rawsort,rlevel,'ta) abstract_argument_type
-val globwit_sort : (rawsort,glevel,'ta) abstract_argument_type
-val wit_sort : (sorts,tlevel,'ta) abstract_argument_type
+val rawwit_sort : (rawsort,rlevel) abstract_argument_type
+val globwit_sort : (rawsort,glevel) abstract_argument_type
+val wit_sort : (sorts,tlevel) abstract_argument_type
 
-val rawwit_constr : (constr_expr,rlevel,'ta) abstract_argument_type
-val globwit_constr : (rawconstr_and_expr,glevel,'ta) abstract_argument_type
-val wit_constr : (constr,tlevel,'ta) abstract_argument_type
+val rawwit_constr : (constr_expr,rlevel) abstract_argument_type
+val globwit_constr : (rawconstr_and_expr,glevel) abstract_argument_type
+val wit_constr : (constr,tlevel) abstract_argument_type
 
-val rawwit_constr_may_eval : ((constr_expr,reference) may_eval,rlevel,'ta) abstract_argument_type
-val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,glevel,'ta) abstract_argument_type
-val wit_constr_may_eval : (constr,tlevel,'ta) abstract_argument_type
+val rawwit_constr_may_eval : ((constr_expr,reference) may_eval,rlevel) abstract_argument_type
+val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,glevel) abstract_argument_type
+val wit_constr_may_eval : (constr,tlevel) abstract_argument_type
 
-val rawwit_open_constr_gen : bool -> (open_constr_expr,rlevel,'ta) abstract_argument_type
-val globwit_open_constr_gen : bool -> (open_rawconstr,glevel,'ta) abstract_argument_type
-val wit_open_constr_gen : bool -> (open_constr,tlevel,'ta) abstract_argument_type
+val rawwit_open_constr_gen : bool -> (open_constr_expr,rlevel) abstract_argument_type
+val globwit_open_constr_gen : bool -> (open_rawconstr,glevel) abstract_argument_type
+val wit_open_constr_gen : bool -> (open_constr,tlevel) abstract_argument_type
 
-val rawwit_open_constr : (open_constr_expr,rlevel,'ta) abstract_argument_type
-val globwit_open_constr : (open_rawconstr,glevel,'ta) abstract_argument_type
-val wit_open_constr : (open_constr,tlevel,'ta) abstract_argument_type
+val rawwit_open_constr : (open_constr_expr,rlevel) abstract_argument_type
+val globwit_open_constr : (open_rawconstr,glevel) abstract_argument_type
+val wit_open_constr : (open_constr,tlevel) abstract_argument_type
 
-val rawwit_casted_open_constr : (open_constr_expr,rlevel,'ta) abstract_argument_type
-val globwit_casted_open_constr : (open_rawconstr,glevel,'ta) abstract_argument_type
-val wit_casted_open_constr : (open_constr,tlevel,'ta) abstract_argument_type
+val rawwit_casted_open_constr : (open_constr_expr,rlevel) abstract_argument_type
+val globwit_casted_open_constr : (open_rawconstr,glevel) abstract_argument_type
+val wit_casted_open_constr : (open_constr,tlevel) abstract_argument_type
 
-val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel,'ta) abstract_argument_type
-val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,glevel,'ta) abstract_argument_type
-val wit_constr_with_bindings : (constr with_bindings,tlevel,'ta) abstract_argument_type
+val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel) abstract_argument_type
+val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,glevel) abstract_argument_type
+val wit_constr_with_bindings : (constr with_bindings,tlevel) abstract_argument_type
 
-val rawwit_bindings : (constr_expr bindings,rlevel,'ta) abstract_argument_type
-val globwit_bindings : (rawconstr_and_expr bindings,glevel,'ta) abstract_argument_type
-val wit_bindings : (constr bindings,tlevel,'ta) abstract_argument_type
+val rawwit_bindings : (constr_expr bindings,rlevel) abstract_argument_type
+val globwit_bindings : (rawconstr_and_expr bindings,glevel) abstract_argument_type
+val wit_bindings : (constr bindings,tlevel) abstract_argument_type
 
-val rawwit_red_expr : ((constr_expr,reference) red_expr_gen,rlevel,'ta) abstract_argument_type
-val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,glevel,'ta) abstract_argument_type
-val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,tlevel,'ta) abstract_argument_type
+val rawwit_red_expr : ((constr_expr,reference) red_expr_gen,rlevel) abstract_argument_type
+val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,glevel) abstract_argument_type
+val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,tlevel) abstract_argument_type
 
 val wit_list0 :
-  ('a,'co,'ta) abstract_argument_type -> ('a list,'co,'ta) abstract_argument_type
+  ('a,'co) abstract_argument_type -> ('a list,'co) abstract_argument_type
 
 val wit_list1 :
-  ('a,'co,'ta) abstract_argument_type -> ('a list,'co,'ta) abstract_argument_type
+  ('a,'co) abstract_argument_type -> ('a list,'co) abstract_argument_type
 
 val wit_opt :
-  ('a,'co,'ta) abstract_argument_type -> ('a option,'co,'ta) abstract_argument_type
+  ('a,'co) abstract_argument_type -> ('a option,'co) abstract_argument_type
 
 val wit_pair :
-  ('a,'co,'ta) abstract_argument_type ->
-  ('b,'co,'ta) abstract_argument_type ->
-      ('a * 'b,'co,'ta) abstract_argument_type
+  ('a,'co) abstract_argument_type ->
+  ('b,'co) abstract_argument_type ->
+      ('a * 'b,'co) abstract_argument_type
 
 (* ['a generic_argument] = (Sigma t:type. t[[constr/'a]]) *)
-type ('a,'b) generic_argument
+type 'a generic_argument
 
 val fold_list0 : 
- (('a,'b) generic_argument -> 'c -> 'c) -> ('a,'b) generic_argument -> 'c -> 'c
+ ('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c
 
 val fold_list1 : 
- (('a,'b) generic_argument -> 'c -> 'c) -> ('a,'b) generic_argument -> 'c -> 'c
+ ('a generic_argument -> 'c -> 'c) -> 'a generic_argument -> 'c -> 'c
 
 val fold_opt :
- (('a,'b) generic_argument -> 'c) -> 'c -> ('a,'b) generic_argument -> 'c
+ ('a generic_argument -> 'c) -> 'c -> 'a generic_argument -> 'c
 
 val fold_pair :
- (('a,'b) generic_argument -> ('a,'b) generic_argument -> 'c) -> 
-      ('a,'b) generic_argument -> 'c
+ ('a generic_argument -> 'a generic_argument -> 'c) -> 
+      'a generic_argument -> 'c
 
 (* [app_list0] fails if applied to an argument not of tag [List0 t]
     for some [t]; it's the responsability of the caller to ensure it *)
 
-val app_list0 : (('a,'b) generic_argument -> ('c,'d) generic_argument) -> 
-('a,'b) generic_argument -> ('c,'d) generic_argument
+val app_list0 : ('a generic_argument -> 'b generic_argument) -> 
+'a generic_argument -> 'b generic_argument
 
-val app_list1 : (('a,'b) generic_argument -> ('c,'d) generic_argument) -> 
-('a,'b) generic_argument -> ('c,'d) generic_argument
+val app_list1 : ('a generic_argument -> 'b generic_argument) -> 
+'a generic_argument -> 'b generic_argument
 
-val app_opt : (('a,'b) generic_argument -> ('c,'d) generic_argument) -> 
-('a,'b) generic_argument -> ('c,'d) generic_argument
+val app_opt : ('a generic_argument -> 'b generic_argument) -> 
+'a generic_argument -> 'b generic_argument
 
 val app_pair :
-  (('a,'b) generic_argument -> ('c,'d) generic_argument) ->
-      (('a,'b) generic_argument -> ('c,'d) generic_argument)
-   -> ('a,'b) generic_argument -> ('c,'d) generic_argument
+  ('a generic_argument -> 'b generic_argument) ->
+      ('a generic_argument -> 'b generic_argument)
+   -> 'a generic_argument -> 'b generic_argument
 
-(* Manque l'ordre supérieur, on aimerait ('co,'ta) 'a; manque aussi le
-   polymorphism, on aimerait que 'b et 'c restent polymorphes à l'appel
-   de create *)
+(* create a new generic type of argument: force to associate
+   unique ML types at each of the three levels *)
 val create_arg : string ->
-      ('a,tlevel,'ta) abstract_argument_type
-      * ('globa,glevel,'globta) abstract_argument_type
-      * ('rawa,rlevel,'rawta) abstract_argument_type
+      ('a,tlevel) abstract_argument_type
+      * ('globa,glevel) abstract_argument_type
+      * ('rawa,rlevel) abstract_argument_type
 
 val exists_argtype : string -> bool
 
@@ -254,15 +266,21 @@ type argument_type =
   | PairArgType of argument_type * argument_type
   | ExtraArgType of string
 
-val genarg_tag : ('a,'b) generic_argument -> argument_type
+val genarg_tag : 'a generic_argument -> argument_type
 
-val unquote : ('a,'co,'ta) abstract_argument_type -> argument_type
+val unquote : ('a,'co) abstract_argument_type -> argument_type
 
-(* We'd like
+val in_gen :
+  ('a,'co) abstract_argument_type -> 'a -> 'co generic_argument
+val out_gen :
+  ('a,'co) abstract_argument_type -> 'co generic_argument -> 'a 
+
+
+(* [in_generic] is used in combination with camlp4 [Gramext.action] magic
 
-  [in_generic: !b:type, !a:argument_type -> (f a) -> b generic_argument]
+   [in_generic: !l:type, !a:argument_type -> |a|_l -> 'l generic_argument]
 
-   with f a = b if a is Constr, f a = c if a is Tactic, otherwise f a = |a|
+   where |a|_l is the interpretation of a at level l
 
    [in_generic] is not typable; we replace the second argument by an absurd
    type (with no introduction rule)
@@ -270,9 +288,4 @@ val unquote : ('a,'co,'ta) abstract_argument_type -> argument_type
 type an_arg_of_this_type
 
 val in_generic : 
-  argument_type -> an_arg_of_this_type -> ('a,'b) generic_argument
-
-val in_gen :
-  ('a,'co,'ta) abstract_argument_type -> 'a -> ('co,'ta) generic_argument
-val out_gen :
-  ('a,'co,'ta) abstract_argument_type -> ('co,'ta) generic_argument -> 'a 
+  argument_type -> an_arg_of_this_type -> 'co generic_argument
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index b0f997d24e..a797275392 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -77,7 +77,7 @@ val force_entry_type :
 
 val create_constr_entry :
   string * gram_universe -> string -> constr_expr Gram.Entry.e
-val create_generic_entry : string -> ('a, rlevel,raw_tactic_expr) abstract_argument_type -> 'a Gram.Entry.e
+val create_generic_entry : string -> ('a, rlevel) abstract_argument_type -> 'a Gram.Entry.e
 val get_generic_entry : string -> grammar_object Gram.Entry.e
 val get_generic_entry_type : string * gram_universe -> string -> Genarg.argument_type
 
@@ -85,33 +85,33 @@ val get_generic_entry_type : string * gram_universe -> string -> Genarg.argument
 
 val tactic_main_level : int
 
-val rawwit_tactic : int -> (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
-val globwit_tactic : int -> (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
-val wit_tactic : int -> (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+val rawwit_tactic : int -> (raw_tactic_expr,rlevel) abstract_argument_type
+val globwit_tactic : int -> (glob_tactic_expr,glevel) abstract_argument_type
+val wit_tactic : int -> (glob_tactic_expr,tlevel) abstract_argument_type
 
-val rawwit_tactic0 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
-val globwit_tactic0 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
-val wit_tactic0 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+val rawwit_tactic0 : (raw_tactic_expr,rlevel) abstract_argument_type
+val globwit_tactic0 : (glob_tactic_expr,glevel) abstract_argument_type
+val wit_tactic0 : (glob_tactic_expr,tlevel) abstract_argument_type
 
-val rawwit_tactic1 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
-val globwit_tactic1 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
-val wit_tactic1 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+val rawwit_tactic1 : (raw_tactic_expr,rlevel) abstract_argument_type
+val globwit_tactic1 : (glob_tactic_expr,glevel) abstract_argument_type
+val wit_tactic1 : (glob_tactic_expr,tlevel) abstract_argument_type
 
-val rawwit_tactic2 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
-val globwit_tactic2 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
-val wit_tactic2 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+val rawwit_tactic2 : (raw_tactic_expr,rlevel) abstract_argument_type
+val globwit_tactic2 : (glob_tactic_expr,glevel) abstract_argument_type
+val wit_tactic2 : (glob_tactic_expr,tlevel) abstract_argument_type
 
-val rawwit_tactic3 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
-val globwit_tactic3 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
-val wit_tactic3 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+val rawwit_tactic3 : (raw_tactic_expr,rlevel) abstract_argument_type
+val globwit_tactic3 : (glob_tactic_expr,glevel) abstract_argument_type
+val wit_tactic3 : (glob_tactic_expr,tlevel) abstract_argument_type
 
-val rawwit_tactic4 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
-val globwit_tactic4 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
-val wit_tactic4 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+val rawwit_tactic4 : (raw_tactic_expr,rlevel) abstract_argument_type
+val globwit_tactic4 : (glob_tactic_expr,glevel) abstract_argument_type
+val wit_tactic4 : (glob_tactic_expr,tlevel) abstract_argument_type
 
-val rawwit_tactic5 : (raw_tactic_expr,rlevel,raw_tactic_expr) abstract_argument_type
-val globwit_tactic5 : (glob_tactic_expr,glevel,glob_tactic_expr) abstract_argument_type
-val wit_tactic5 : (glob_tactic_expr,tlevel,glob_tactic_expr) abstract_argument_type
+val rawwit_tactic5 : (raw_tactic_expr,rlevel) abstract_argument_type
+val globwit_tactic5 : (glob_tactic_expr,glevel) abstract_argument_type
+val wit_tactic5 : (glob_tactic_expr,tlevel) abstract_argument_type
 
 val is_tactic_genarg : argument_type -> bool
 
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 451313be5a..ebf4b5ad1c 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -129,7 +129,7 @@ let rec pr_message_token prid = function
 
 let pr_fresh_ids = prlist (fun s -> spc() ++ pr_or_var qs s)
 
-let rec pr_raw_generic prc prlc prtac prref (x:(Genarg.rlevel, Tacexpr.raw_tactic_expr) Genarg.generic_argument) =
+let rec pr_raw_generic prc prlc prtac prref (x:Genarg.rlevel Genarg.generic_argument) =
   match Genarg.genarg_tag x with
   | BoolArgType -> pr_arg str (if out_gen rawwit_bool x then "true" else "false")
   | IntArgType -> pr_arg int (out_gen rawwit_int x)
diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli
index 7b546b2906..993f1ae622 100644
--- a/parsing/pptactic.mli
+++ b/parsing/pptactic.mli
@@ -58,9 +58,8 @@ val pr_raw_generic :
   (constr_expr -> std_ppcmds) ->
   (constr_expr -> std_ppcmds) ->
   (tolerability -> raw_tactic_expr -> std_ppcmds) ->
-  (Libnames.reference -> std_ppcmds) ->
-    (constr_expr, raw_tactic_expr) generic_argument ->
-      std_ppcmds
+  (Libnames.reference -> std_ppcmds) -> constr_expr generic_argument ->
+    std_ppcmds
 
 val pr_raw_extend:
   (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) ->
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 662b268f64..d7a9879be7 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -188,11 +188,11 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis
       
   (* For ML extensions *)
-  | TacExtend of loc * string * ('constr,'tac) generic_argument list
+  | TacExtend of loc * string * 'constr generic_argument list
 
   (* For syntax extensions *)
   | TacAlias of loc * string *
-      (identifier * ('constr,'tac) generic_argument) list
+      (identifier * 'constr generic_argument) list
       * (dir_path * glob_tactic_expr)
 
 and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr =
@@ -221,7 +221,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr =
 and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast =
   identifier option list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
 
-  (* These are possible arguments of a tactic definition *)
+  (* These are the possible arguments of a tactic definition *)
 and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg =
   | TacDynamic     of loc * Dyn.t
   | TacVoid
@@ -274,8 +274,7 @@ type raw_tactic_arg =
      identifier located or_metaid,
      raw_tactic_expr) gen_tactic_arg
 
-type raw_generic_argument =
-    (constr_expr,raw_tactic_expr) generic_argument
+type raw_generic_argument = constr_expr generic_argument
 
 type raw_red_expr = (constr_expr, reference) red_expr_gen
 
@@ -297,28 +296,21 @@ type glob_tactic_arg =
      identifier located,
      glob_tactic_expr) gen_tactic_arg
 
-type glob_generic_argument =
-    (rawconstr_and_expr,glob_tactic_expr) generic_argument
+type glob_generic_argument = rawconstr_and_expr generic_argument
 
 type glob_red_expr =
     (rawconstr_and_expr, evaluable_global_reference or_var) red_expr_gen
 
-type closed_raw_generic_argument =
-    (constr_expr,raw_tactic_expr) generic_argument
+type closed_raw_generic_argument = constr_expr generic_argument
 
-type 'a raw_abstract_argument_type =
-    ('a,rlevel,raw_tactic_expr) abstract_argument_type
+type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type
 
-type 'a glob_abstract_argument_type =
-    ('a,glevel,glob_tactic_expr) abstract_argument_type
+type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type
 
-type open_generic_argument =
-    (Term.constr,glob_tactic_expr) generic_argument
+type open_generic_argument = Term.constr generic_argument
 
-type closed_generic_argument =
-    (Term.constr,glob_tactic_expr) generic_argument
+type closed_generic_argument = Term.constr generic_argument
 
-type 'a closed_abstract_argument_type =
-    ('a,Term.constr,glob_tactic_expr) abstract_argument_type
+type 'a closed_abstract_argument_type = ('a,Term.constr) abstract_argument_type
 
 type declaration_hook = Decl_kinds.strength -> global_reference -> unit