Correction de bugs lié au commit 10124 (décalage des indices de Bruijn)

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

3 files changed, 38 insertions, 5 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 87fea20383..ab3e655a13 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -387,7 +387,7 @@ let extend_evar env evdref k (evk1,args1) c =
   let filter = if List.for_all (fun x -> x) filter then None else Some filter in
   let evar1' = e_new_evar evdref extenv ~filter:filter ty in
   let evk1',args1'_in_env = destEvar evar1' in
-  let args1'_in_extenv = overwrite_first args1'_in_env (Array.map (lift k) args1) in
+  let args1'_in_extenv = Array.map (lift k) (overwrite_first args1'_in_env args1) in
   (evar1',(evk1',args1'_in_extenv))
 
 let subfilter p filter l =
@@ -776,6 +776,7 @@ let rec invert_instance env evd (evk,_ as ev) subst rhs =
     | Var id -> project_variable env' t k t
     | Evar (evk',args' as ev') ->
 	(* Evar/Evar problem (but left evar is virtual) *)
+	let subst = List.map (fun (id,(idc,c)) -> (id,(idc,lift k c))) subst in
 	let projs' =
 	  array_map_to_list (invert_subst env (evars_of !evdref) subst) args'
 	in
@@ -796,10 +797,10 @@ let rec invert_instance env evd (evk,_ as ev) subst rhs =
 	  let (evar'',ev'') = extend_evar env' evdref k ev t in
 	  let evd =
 	    (* Try to project (a restriction of) the left evar ... *)
-	    try solve_evar_evar_l2r evar_define env !evdref ev'' ev t
+	    try solve_evar_evar_l2r evar_define env' !evdref ev'' ev t
 	    with CannotProject filter'' ->
 	    (* ... or postpone the problem *)
-	    postpone_evar_evar env !evdref filter'' ev'' filter' ev' in
+	    postpone_evar_evar env' !evdref filter'' ev'' filter' ev' in
 	  evdref := evd;
 	  evar'')
     | _ ->
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 94b3d9e06c..06b3a542d7 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -616,10 +616,15 @@ let pr_meta_map mmap =
   in
   prlist pr_meta_binding (metamap_to_list mmap)
 
-let pr_idl idl = prlist_with_sep pr_spc pr_id idl
+let pr_decl ((id,b,_),ok) =
+  match b with
+  | None -> if ok then pr_id id else (str "{" ++ pr_id id ++ str "}")
+  | Some c -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++ 
+      print_constr c ++ str (if ok then ")" else "}")
 
 let pr_evar_info evi =
-  let phyps = pr_idl (List.rev (ids_of_named_context (evar_context evi))) in
+  let decls = List.combine (evar_context evi) (evar_filter evi) in
+  let phyps = prlist_with_sep pr_spc pr_decl (List.rev decls) in
   let pty = print_constr evi.evar_concl in
   let pb =
     match evi.evar_body with
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 94daad3a59..27470730d2 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -109,6 +109,7 @@ Variables elt elt': Set.
 Definition map' f (m:t' elt) : t' elt' := 
   Bbst (map_bst f m.(is_bst)) (map_avl f m.(is_avl)).
 End B.
+Unset Implicit Arguments.
 
 (* An example from Lexicographic_Exponentiation that tests the 
    contraction of reducible fixpoints in type inference *)
@@ -123,3 +124,29 @@ Check (fun (A:Set) (a b x:A) (l:list A)
 Parameter g:(nat->nat)->(nat->nat).
 Fixpoint G p cont {struct p} :=
   g (fun n => match p with O => cont | S p => G p cont end n).
+
+(* An example from Bordeaux/Cantor that applies evar restriction 
+   below  a binder *)
+
+Require Import Relations.
+Parameter lex : forall (A B : Set), (forall (a1 a2:A), {a1=a2}+{a1<>a2})
+-> relation A -> relation B -> A * B -> A * B -> Prop.
+Check 
+ forall (A B : Set) eq_A_dec o1 o2, 
+ antisymmetric A o1 -> transitive A o1 -> transitive B o2 ->
+ transitive _ (lex _ _ eq_A_dec o1 o2).
+
+(* Another example from Julien Forest that tests unification below binders *)
+
+Require Import List.
+Set Implicit Arguments.
+Parameter
+ merge : forall (A B : Set) (eqA : forall (a1 a2 : A), {a1=a2}+{a1<>a2})
+                         (eqB : forall (b1 b2 : B), {b1=b2}+{b1<>b2})
+                        (partial_res l : list (A*B)), option (list (A*B)).
+Axiom merge_correct :
+   forall (A B : Set) eqA eqB (l1 l2 : list (A*B)),
+       (forall a2 b2 c2, In (a2,b2) l2 -> In (a2,c2) l2 -> b2 = c2) ->
+       match merge eqA eqB l1 l2 with _ => True end.
+Unset Implicit Arguments.
+