Prise en compte des Let dans l'instance des evars

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

2 files changed, 22 insertions, 6 deletions

diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 27754ae841..c73fbd220d 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -24,7 +24,22 @@ let instantiate sign c args =
   else
     replace_vars inst c
 
-let instantiate_evar = instantiate
+(* Vérifier que les instances des let-in sont compatibles ?? *)
+let instantiate_sign_including_let sign args =
+  let rec instrec = function
+    | ((id,b,_) :: sign, c::args) -> (id,c) :: (instrec (sign,args))
+    | ([],[])                        -> []
+    | ([],_) | (_,[]) ->
+    anomaly "Signature and its instance do not match"
+  in 
+  instrec (sign,args)
+
+let instantiate_evar sign c args =
+  let inst = instantiate_sign_including_let sign args in
+  if is_id_inst inst then
+    c
+  else
+    replace_vars inst c
 
 let instantiate_constr sign c args =
   if Options.immediate_discharge then
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index c155c45554..d7df2507cd 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -61,7 +61,7 @@ let dummy_sort = mkType dummy_univ
 
 let make_evar_instance env =
   fold_named_context
-    (fun env (id, b, _) l -> if b=None then mkVar id :: l else l)
+    (fun env (id, b, _) l -> (*if b=None then*) mkVar id :: l (*else l*))
     env []
 
 (* Declaring any type to be in the sort Type shouldn't be harmful since
@@ -189,6 +189,7 @@ let real_clean isevars sp args rhs =
 	    else begin
 	      let (sigma,rc) = do_restrict_hyps !isevars ev args' in
 	      isevars := sigma;
+
 	      rc
 	    end
 	  else
@@ -204,18 +205,18 @@ let make_evar_instance_with_rel env =
   let n = rel_context_length (rel_context env) in
   let vars = 
     fold_named_context
-      (fun env (id,b,_) l -> if b=None then mkVar id :: l else l)
+      (fun env (id,b,_) l -> (* if b=None then *) mkVar id :: l (*else l*))
       env [] in
   snd (fold_rel_context
-    (fun env (_,b,_) (i,l) -> (i-1, if b=None then mkRel i :: l else l))
+    (fun env (_,b,_) (i,l) -> (i-1, (*if b=None then *) mkRel i :: l (*else l*)))
     env (n,vars))
 
 let make_subst env args =
   snd (fold_named_context
     (fun env (id,b,c) (args,l as g) ->
        match b, args with
-	 | None, a::rest -> (rest, (id,a)::l)
-	 | Some _, _ -> g
+	 | (* None *) _ , a::rest -> (rest, (id,a)::l)
+(*	 | Some _, _ -> g*)
 	 | _ -> anomaly "Instance does not match its signature")
     env (List.rev args,[]))