Type inference unification: fixed a 8.4 bug in the presence of unification

with evars under binders.

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

2 files changed, 63 insertions, 2 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 7d66bee053..9ff40c54ca 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -490,10 +490,13 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
             define_evar_from_virtual_equation define_fun env evd t_in_env
               sign filter inst_in_env inst_in_sign in
           (push_named_context_val (id,None,t_in_sign) sign,true::filter,
-           (mkRel 1)::(List.map (lift 1) inst_in_env),(mkVar id)::inst_in_sign,
+           (mkRel 1)::(List.map (lift 1) inst_in_env),
+           (mkRel 1)::(List.map (lift 1) inst_in_sign),
            push_rel d env,evd,id::avoid)
       | Some b ->
-          (sign,filter,inst_in_env,inst_in_sign,
+          (sign,filter,
+           List.map (lift 1) inst_in_env,
+           List.map (lift 1) inst_in_sign,
            push_rel d env,evd,avoid))
       rel_sign
       (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1)
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 2f1ec75716..906eb0fc9a 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -309,3 +309,61 @@ Definition k6
 Definition k7
   (e:forall P : nat -> Prop, (exists n : nat, let n' := n in P n') -> nat)
   (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j b).
+
+(* An example that uses materialize_evar under binders *)
+(* Extracted from bigop.v in the mathematical components library *)
+
+Section Bigop.
+
+Variable bigop : forall R I: Type,
+  R -> (R -> R -> R) -> list I -> (I->Prop) -> (I -> R) -> R.
+
+Hypothesis eq_bigr :
+forall (R : Type) (idx : R) (op : R -> R -> R)
+       (I : Type) (r : list I) (P : I -> Prop) (F1 F2 : I -> R),
+       (forall i : I, P i -> F1 i = F2 i) ->
+       bigop R I idx op r (fun i : I => P i) (fun i : I => F1 i) = idx.
+
+Hypothesis big_tnth :
+forall (R : Type) (idx : R) (op : R -> R -> R)
+     (I : Type) (r : list I) (P : I -> Prop) (F : I -> R),
+     bigop R I idx op r (fun i : I => P i) (fun i : I => F i) = idx.
+
+Hypothesis big_tnth_with_letin :
+forall (R : Type) (idx : R) (op : R -> R -> R)
+     (I : Type) (r : list I) (P : I -> Prop) (F : I -> R),
+     bigop R I idx op r (fun i : I => let i:=i in P i) (fun i : I => F i) = idx.
+
+Variable R : Type.
+Variable idx : R.
+Variable op : R -> R -> R.
+Variable I : Type.
+Variable J : Type.
+Variable rI : list I.
+Variable rJ : list J.
+Variable xQ : J -> Prop.
+Variable P : I -> Prop.
+Variable Q : I -> J -> Prop.
+Variable F : I -> J -> R.
+
+(* Check unification under binders *)
+
+Check (eq_bigr _ _ _ _ _ _ _ _ (fun _ _ => big_tnth _ _ _ _ rI _ _))
+  : (bigop R J idx op rJ
+        (fun j : J => let k:=j in xQ k)
+        (fun j : J => let k:=j in 
+         bigop R I idx
+           op rI
+           (fun i : I => P i /\ Q i k) (fun i : I => let k:=j in F i k))) = idx.
+
+(* Check also with let-in *)
+
+Check (eq_bigr _ _ _ _ _ _ _ _ (fun _ _ => big_tnth_with_letin _ _ _ _ rI _ _))
+  : (bigop R J idx op rJ
+        (fun j : J => let k:=j in xQ k)
+        (fun j : J => let k:=j in 
+         bigop R I idx
+           op rI
+           (fun i : I => P i /\ Q i k) (fun i : I => let k:=j in F i k))) = idx.
+
+End Bigop.