blob: a6113ab9a1394b77174a63afbaabbf63f354315a (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
(* Check dependencies in the matching predicate (was failing in V8.0pl1) *)
Inductive t : forall x : 0 = 0, x = x -> Prop :=
c : forall x : 0 = 0, t x (refl_equal x).
Definition a (x : t _ (refl_equal (refl_equal 0))) :=
match x return match x with
| c y => Prop
end with
| c y => y = y
end.
|
