Branchement du mécanisme d'instantiation des Evar en présence de définitions locales vers Evarutil

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

3 files changed, 12 insertions, 9 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index f4cc94fd6a..7e2d151bd7 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -59,7 +59,7 @@ let new_isevar_sign env sigma typ instance =
    any type has type Type. May cause some trouble, but not so far... *)
 let dummy_sort = mkType dummy_univ
 
-let make_instance env =
+let make_evar_instance env =
   fold_named_context
     (fun env (id, b, _) l -> if b=None then mkVar id :: l else l)
     env []
@@ -67,7 +67,7 @@ let make_instance env =
 (* Declaring any type to be in the sort Type shouldn't be harmful since
    cumulativity now includes Prop and Set in Type. *)
 let new_type_var env sigma =
-  let instance = make_instance env in
+  let instance = make_evar_instance env in
   let (sigma',c) = new_isevar_sign env sigma dummy_sort instance in
   (sigma', c)
 
@@ -115,7 +115,7 @@ let do_restrict_hyps sigma c =
   in
   let sign' = List.rev rsign in
   let env' = change_hyps (fun _ -> sign') env in
-  let instance = make_instance env' in
+  let instance = make_evar_instance env' in
   let (sigma',nc) = new_isevar_sign env' sigma evd.evar_concl instance in
   let sigma'' = Evd.define sigma' ev nc in
   (sigma'', nc)
@@ -194,7 +194,7 @@ let real_clean isevars sp args rhs =
   (* if not (closed0 body) then error_not_clean CCI empty_env sp body; *)
   body
 
-let make_instance_with_rel env =
+let make_evar_instance_with_rel env =
   let n = rel_context_length (rel_context env) in
   let vars = 
     fold_named_context
@@ -219,7 +219,7 @@ let make_subst env args =
 let new_isevar isevars env typ k =
   let subst,env' = push_rel_context_to_named_context env in
   let typ' = substl subst typ in
-  let instance = make_instance_with_rel env in
+  let instance = make_evar_instance_with_rel env in
   let (sigma',evar) = new_isevar_sign env' !isevars typ' instance in
   isevars := sigma';
   evar
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 6e70539cac..753bb0fd18 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -25,6 +25,8 @@ val ise_try : 'a evar_defs -> (unit -> bool) list -> bool
 val ise_undefined : 'a evar_defs -> constr -> bool
 val has_undefined_isevars : 'a evar_defs -> constr -> bool
 
+val make_evar_instance : env -> constr list
+
 val new_isevar : 'a evar_defs -> env -> constr -> path_kind -> constr
 
 val is_eliminator : constr -> bool
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 1332e0ecdb..5ce77f413d 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -32,9 +32,8 @@ type 'a clausenv = {
 type wc = walking_constraints
 
 let new_evar_in_sign env =
-  let ids = ids_of_named_context (Environ.named_context env) in
   let ev = new_evar () in
-  mkEvar (ev, Array.of_list (List.map mkVar ids))
+  mkEvar (ev, Array.of_list (Evarutil.make_evar_instance env))
 
 let rec whd_evar sigma t = match kind_of_term t with
   | IsEvar (ev,_ as evc) when is_defined sigma ev ->
@@ -127,17 +126,19 @@ let unify_0 mc wc m n =
 	| _, IsEvar _ ->
 	    metasubst,((cN,cM)::evarsubst)
 
-	| IsConst _, _ ->
+	| (IsConst _ | IsVar _ | IsRel _), _ ->
 	    if is_conv env sigma cM cN then
 	      substn
 	    else 
 	      error_cannot_unify CCI (m,n)
 		
-	| _, IsConst _ ->
+	| _, (IsConst _ | IsVar _| IsRel _) ->
 	    if (not (occur_meta cM)) & is_conv env sigma cM cN then 
 	      substn
 	    else 
 	      error_cannot_unify CCI (m,n)
+
+	| IsLetIn (_,b,_,c), _ -> unirec_rec substn (subst1 b c) cN
 		
 	| _ -> error_cannot_unify CCI (m,n)