Plus d'uniformite dans la gestion des implicites d'inductifs; nouvelles entrees pour Metasyntax

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

2 files changed, 32 insertions, 20 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 268aacd40..66851e70e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -22,10 +22,12 @@ open Topconstr
 open Nametab
 open Symbols
 
-type implicits_env = (* For interpretation of inductive type with implicits *)
-    identifier list * 
+type implicits_env = (* To interpret inductive type with implicits *)
     (identifier * (identifier list * Impargs.implicits_list)) list
 
+type full_implicits_env =
+    identifier list * implicits_env
+
 let interning_grammar = ref false
 
 let for_grammar f x =
@@ -161,17 +163,17 @@ let set_var_scope loc id (_,scopt,scopes) (_,_,varscopes,_,_) =
    abstracted until this point *)
 
 let intern_var (env,_,_) ((vars1,unbndltacvars),vars2,_,_,impls) loc id =
+  (* Is [id] an inductive type potentially with implicit *)
+  try
+    let l,impl = List.assoc id impls in
+    let l = List.map 
+      (fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in
+    RVar (loc,id), impl, [],
+    (if !Options.v7 & !interning_grammar then [] else l)
+  with Not_found ->
   (* Is [id] bound in current env or ltac vars bound to constr *)
   if Idset.mem id env or List.mem id vars1
   then
-    (* Is [id] an inductive type with implicit *)
-    try
-      let l,impl = List.assoc id impls in
-      let l = List.map 
-	(fun id -> CRef (Ident (loc,id)), Some (loc,ExplByName id)) l in
-      RVar (loc,id), impl, [],
-      (if !Options.v7 & !interning_grammar then [] else l)
-    with Not_found ->
       RVar (loc,id), [], [], []
   else
   (* Is [id] bound to a free name in ltac (this is an ltac error message) *)
@@ -412,10 +414,10 @@ let locate_if_isevar loc na = function
       with Not_found -> RHole (loc, BinderType na))
   | x -> x
 
-let check_hidden_implicit_parameters id (_,_,_,indparams,_) =
-  if List.mem id indparams then
-    errorlabstrm "" (str "A parameter of inductive type " ++ pr_id id
-      ++ str " must not be used as a bound variable in the type \
+let check_hidden_implicit_parameters id (_,_,_,indnames,_) =
+  if List.mem id indnames then
+    errorlabstrm "" (str "A parameter or name of an inductive type " ++
+    pr_id id ++ str " must not be used as a bound variable in the type \
 of its constructor")
 
 let push_name_env lvar (ids,tmpsc,scopes as env) = function
@@ -795,6 +797,10 @@ let interp_rawtype sigma env c =
 let interp_rawtype_with_implicits sigma env impls c =
   interp_rawconstr_gen_with_implicits true sigma env impls false ([],[]) c
 
+let interp_rawconstr_with_implicits env vars impls c =
+  interp_rawconstr_gen_with_implicits false Evd.empty env ([],impls) false
+    (vars,[]) c
+
 (*
 (* The same as interp_rawconstr but with a list of variables which must not be
    globalized *)
@@ -872,12 +878,12 @@ let interp_constrpattern_gen sigma env ltacvar c =
 let interp_constrpattern sigma env c =
   interp_constrpattern_gen sigma env [] c
 
-let interp_aconstr vars a =
+let interp_aconstr impls vars a =
   let env = Global.env () in
   (* [vl] is intended to remember the scope of the free variables of [a] *)
   let vl = List.map (fun id -> (id,ref None)) vars in
   let c = for_grammar (internalise Evd.empty (extract_ids env, None, [])
-    false (([],[]),Environ.named_context env,vl,[],[])) a in
+    false (([],[]),Environ.named_context env,vl,[],impls)) a in
   (* Translate and check that [c] has all its free variables bound in [vars] *)
   let a = aconstr_of_rawconstr vars c in
   (* Returns [a] and the ordered list of variables with their scopes *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index fa7162435..c1c9ede02 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -33,10 +33,12 @@ open Termops
    - insert existential variables for implicit arguments
 *)
 
-type implicits_env = (* For interpretation of inductive type with implicits *)
-    identifier list * 
+type implicits_env = (* To interpret inductive type with implicits *)
     (identifier * (identifier list * Impargs.implicits_list)) list
 
+type full_implicits_env =
+    identifier list * implicits_env
+
 type ltac_sign = 
   identifier list * (identifier * identifier option) list
 
@@ -62,7 +64,10 @@ val interp_casted_openconstr    :
    argument associates a list of implicit positions to identifiers
    declared in the rel_context of [env] *)
 val interp_type_with_implicits : 
-  evar_map -> env -> implicits_env -> constr_expr -> types
+  evar_map -> env -> full_implicits_env -> constr_expr -> types
+
+val interp_rawconstr_with_implicits :
+  env -> identifier list -> implicits_env -> constr_expr -> rawconstr
 
 (*s Build a judgement from *)
 val judgment_of_rawconstr : evar_map -> env -> constr_expr -> unsafe_judgment
@@ -91,7 +96,8 @@ val interp_constrpattern :
 val interp_reference : ltac_sign -> reference -> rawconstr
 
 (* Interprets into a abbreviatable constr *)
-val interp_aconstr : identifier list -> constr_expr -> interpretation
+val interp_aconstr : implicits_env -> identifier list -> constr_expr ->
+  interpretation
 
 (* Globalization leak for Grammar *)
 val for_grammar : ('a -> 'b) -> 'a -> 'b