From af22eb086aaec3551ccc9dd6bcf754c38f933eb6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 14 Mar 2001 21:21:12 +0000
Subject: 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
---
 kernel/instantiate.ml | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

(limited to 'kernel')

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