aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Case8.v
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.