From 7b0c76beedf0e4e59c03701ee776a7c1dae58e20 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 27 Nov 2000 10:25:19 +0000
Subject: 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
---
 proofs/clenv.ml | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

(limited to 'proofs')

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)
 	      
-- 
cgit v1.2.3