diff options
| -rw-r--r-- | pretyping/evarutil.ml | 5 | ||||
| -rw-r--r-- | test-suite/success/evars.v | 8 |
2 files changed, 12 insertions, 1 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 58d7ba9d4..993cb3a85 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 52c4f2daa..ba8da1a4f 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. |