Correction trou de subject-reduction de create_arg dans genarg.mli

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

6 files changed, 86 insertions, 71 deletions

diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 2f47608c10..55e60199f4 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -49,11 +49,11 @@ GEXTEND Gram
     ;
   END
 
-type gallina_loc_argtype = (Vernacexpr.vernac_expr located, constr_expr, Tacexpr.raw_tactic_expr) Genarg.abstract_argument_type
+type ('a,'b) gallina_loc_argtype = (Vernacexpr.vernac_expr located, 'a, 'b) Genarg.abstract_argument_type
 
-let (wit_subtac_gallina_loc : gallina_loc_argtype),
-  (globwit_subtac_gallina_loc : gallina_loc_argtype),
-  (rawwit_subtac_gallina_loc : gallina_loc_argtype) =
+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) =
   Genarg.create_arg "subtac_gallina_loc"
 
 VERNAC COMMAND EXTEND Subtac
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 2d51e2a183..294678d484 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -53,6 +53,10 @@ type ('a,'b) generic_argument = argument_type * Obj.t
 
 let dyntab = ref ([] : string list)
 
+type rlevel = constr_expr
+type glevel = rawconstr_and_expr
+type tlevel = constr
+
 type ('a,'b,'c) abstract_argument_type = argument_type
 
 let create_arg s =
diff --git a/interp/genarg.mli b/interp/genarg.mli
index dacafc4571..f82eac0cb7 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -82,88 +82,99 @@ ExtraArgType of string         '_a                      '_b
 \end{verbatim}
 *)
 
+(* 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
+   out_gen is monomorphic over 'a, hence type-safe 
+*)
+
+type rlevel = constr_expr
+type glevel = rawconstr_and_expr
+type tlevel = constr
+
 type ('a,'co,'ta) abstract_argument_type
 
-val rawwit_bool : (bool,'co,'ta) abstract_argument_type
-val globwit_bool : (bool,'co,'ta) abstract_argument_type
-val wit_bool : (bool,'co,'ta) 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_int : (int,'co,'ta) abstract_argument_type
-val globwit_int : (int,'co,'ta) abstract_argument_type
-val wit_int : (int,'co,'ta) 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_or_var : (int or_var,'co,'ta) abstract_argument_type
-val globwit_int_or_var : (int or_var,'co,'ta) abstract_argument_type
-val wit_int_or_var : (int or_var,'co,'ta) 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_string : (string,'co,'ta) abstract_argument_type
-val globwit_string : (string,'co,'ta) abstract_argument_type
-val wit_string : (string,'co,'ta) 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_pre_ident : (string,'co,'ta) abstract_argument_type
-val globwit_pre_ident : (string,'co,'ta) abstract_argument_type
-val wit_pre_ident : (string,'co,'ta) 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_intro_pattern : (intro_pattern_expr,'co,'ta) abstract_argument_type
-val globwit_intro_pattern : (intro_pattern_expr,'co,'ta) abstract_argument_type
-val wit_intro_pattern : (intro_pattern_expr,'co,'ta) 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_ident : (identifier,'co,'ta) abstract_argument_type
-val globwit_ident : (identifier,'co,'ta) abstract_argument_type
-val wit_ident : (identifier,'co,'ta) 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_var : (identifier located,'co,'ta) abstract_argument_type
-val globwit_var : (identifier located,'co,'ta) abstract_argument_type
-val wit_var : (identifier,'co,'ta) 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_ref : (reference,constr_expr,'ta) abstract_argument_type
-val globwit_ref : (global_reference located or_var,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_ref : (global_reference,constr,'ta) 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_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type
-val globwit_quant_hyp : (quantified_hypothesis,'co,'ta) abstract_argument_type
-val wit_quant_hyp : (quantified_hypothesis,'co,'ta) 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_sort : (rawsort,constr_expr,'ta) abstract_argument_type
-val globwit_sort : (rawsort,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_sort : (sorts,constr,'ta) 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_constr : (constr_expr,constr_expr,'ta) abstract_argument_type
-val globwit_constr : (rawconstr_and_expr,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_constr : (constr,constr,'ta) 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_may_eval : ((constr_expr,reference) may_eval,constr_expr,'ta) abstract_argument_type
-val globwit_constr_may_eval : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) may_eval,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_constr_may_eval : (constr,constr,'ta) 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_open_constr_gen : bool -> (open_constr_expr,constr_expr,'ta) abstract_argument_type
-val globwit_open_constr_gen : bool -> (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_open_constr_gen : bool -> (open_constr,constr,'ta) 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 : (open_constr_expr,constr_expr,'ta) abstract_argument_type
-val globwit_open_constr : (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_open_constr : (open_constr,constr,'ta) 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_casted_open_constr : (open_constr_expr,constr_expr,'ta) abstract_argument_type
-val globwit_casted_open_constr : (open_rawconstr,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_casted_open_constr : (open_constr,constr,'ta) 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_constr_with_bindings : (constr_expr with_bindings,constr_expr,'ta) abstract_argument_type
-val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_constr_with_bindings : (constr with_bindings,constr,'ta) 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_bindings : (constr_expr bindings,constr_expr,'ta) abstract_argument_type
-val globwit_bindings : (rawconstr_and_expr bindings,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_bindings : (constr bindings,constr,'ta) 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_red_expr : ((constr_expr,reference) red_expr_gen,constr_expr,'ta) abstract_argument_type
-val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_red_expr : ((constr,evaluable_global_reference) red_expr_gen,constr,'ta) 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
 
 (* TODO: transformer tactic en extra arg *)
-val rawwit_tactic : int -> ('ta,constr_expr,'ta) abstract_argument_type
-val globwit_tactic : int -> ('ta,rawconstr_and_expr,'ta) abstract_argument_type
-val wit_tactic : int -> ('ta,constr,'ta) abstract_argument_type
+val rawwit_tactic : int -> ('ta,rlevel,'ta) abstract_argument_type
+val globwit_tactic : int -> ('ta,glevel,'ta) abstract_argument_type
+val wit_tactic : int -> ('ta,tlevel,'ta) abstract_argument_type
 
 val wit_list0 :
   ('a,'co,'ta) abstract_argument_type -> ('a list,'co,'ta) abstract_argument_type
@@ -216,9 +227,9 @@ val app_pair :
    polymorphism, on aimerait que 'b et 'c restent polymorphes à l'appel
    de create *)
 val create_arg : string ->
-      ('a,'co,'ta) abstract_argument_type
-      * ('globa,'globco,'globta) abstract_argument_type
-      * ('rawa,'rawco,'rawta) abstract_argument_type
+      ('a,tlevel,'ta) abstract_argument_type
+      * ('globa,glevel,'globta) abstract_argument_type
+      * ('rawa,rlevel,'rawta) abstract_argument_type
 
 val exists_argtype : string -> bool
 
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 46ecd11d24..690810d8ab 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, constr_expr,raw_tactic_expr) abstract_argument_type -> 'a Gram.Entry.e
+val create_generic_entry : string -> ('a, rlevel,raw_tactic_expr) 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
 
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 2f86ac94cf..f18bcf414a 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -127,7 +127,7 @@ let rec pr_message_token prid = function
   | MsgInt n -> int n
   | MsgIdent id -> prid id
 
-let rec pr_raw_generic prc prlc prtac prref x =
+let rec pr_raw_generic prc prlc prtac prref (x:(Genarg.rlevel, Tacexpr.raw_tactic_expr) 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/proofs/tacexpr.ml b/proofs/tacexpr.ml
index af3eec9812..1dc822a27c 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -307,10 +307,10 @@ type closed_raw_generic_argument =
     (constr_expr,raw_tactic_expr) generic_argument
 
 type 'a raw_abstract_argument_type =
-    ('a,constr_expr,raw_tactic_expr) abstract_argument_type
+    ('a,rlevel,raw_tactic_expr) abstract_argument_type
 
 type 'a glob_abstract_argument_type =
-    ('a,rawconstr_and_expr,glob_tactic_expr) abstract_argument_type
+    ('a,glevel,glob_tactic_expr) abstract_argument_type
 
 type open_generic_argument =
     (Term.constr,glob_tactic_expr) generic_argument