blob: 54e1a07cc8bd566d474afca8dafa01ec1c1d29f8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
(* This failed with an anomaly in pre-8.4 because of let-in not
properly taken into account in the test for unification pattern *)
Inductive foo : forall A, A -> Prop :=
| foo_intro : forall A x, foo A x.
Lemma bar A B f : foo (A -> B) f -> forall x : A, foo B (f x).
Fail induction 1.
(* Whether these examples should succeed with a non-dependent return predicate
or fail because there is well-typed return predicate dependent in f
is questionable. As of 25 oct 2011, they succeed *)
refine (fun p => match p with _ => _ end).
Undo.
refine (fun p => match p with foo_intro _ _ => _ end).
|
