|
(* 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.
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
