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

2 files changed, 11 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