1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
|
(* 1st-order unification did not work when in competition with pattern unif. *)
Set Implicit Arguments.
Lemma test : forall
(A : Type)
(B : Type)
(f : A -> B)
(S : B -> Prop)
(EV : forall y (f':A->B), (forall x', S (f' x')) -> S (f y))
(HS : forall x', S (f x'))
(x : A),
S (f x).
Proof.
intros. eapply EV. intros.
(* worked in v8.2 but not in v8.3beta, fixed in r12898 *)
apply HS.
(* still not compatible with 8.2 because an evar can be solved in
two different ways and is left open *)
Abort.
|
