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

1 files changed, 16 insertions, 1 deletions

diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index 27754ae84..c73fbd220 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