Fixing another bug revealing ill-typed use of evar restriction.

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

2 files changed, 12 insertions, 1 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 58d7ba9d44..993cb3a850 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1102,10 +1102,13 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
       | NotUniqueInType ty ->
 	  if not !progress then raise NotEnoughInformationToProgress;
 	  (* No unique projection but still restrict to where it is possible *)
+          (* materializing is necessary, but is restricting useful? *)
+	  let (evd,_,ev') =
+            materialize_evar (evar_define conv_algo) env !evdref 0 ev ty in
 	  let ts = expansions_of_var aliases t in
 	  let test c = isEvar c or List.mem c ts in
 	  let filter = array_map_to_list test argsv in
-	  let evarenv,src,filter,_ = restrict_hyps ~refine:true !evdref evk filter in
+	  let evarenv,src,filter,_ = restrict_hyps ~refine:true evd (fst ev') filter in
 	  let args' = filter_along (fun x -> x) filter argsv in
 	  let evd,evar = new_evar !evdref evarenv ~src ~filter ty in
 	  let evk',_ = destEvar evar in
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 52c4f2daad..ba8da1a4f3 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -258,3 +258,11 @@ Abort.
 (* Regression test *)
 
 Definition fo : option nat -> nat := option_rec _ (fun a => 0) 0.
+
+(* This example revealed an incorrect evar restriction at some time
+   around October 2011 *)
+
+Goal forall (A:Type) (a:A) (P:forall A, A -> Prop), (P A a) /\ (P A a).
+intros.
+refine ((fun H => conj (proj1 H) (proj2 H)) _).
+Abort.