aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/success/Case14.v
blob: f106a64cb5e5a1daab4966e537d83e1a77611f44 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
(* Test of inference of elimination predicate for "if" *)
(* submitted by Robert R Schneck *)

Axiom bad : false = true.

Definition try1 : False :=
  match bad in (_ = b) return (if b then False else True) with
  | refl_equal => I
  end.

Definition try2 : False :=
  match bad in (_ = b) return ((if b then False else True):Prop) with
  | refl_equal => I
  end.

Definition try3 : False :=
  match
    bad in (_ = b) return ((fun b' : bool => if b' then False else True) b)
  with
  | refl_equal => I
  end.