aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/Case2.v
blob: 7d81ee81bf232fa0553635649f51a50bfa85abbf (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
Inductive IFExpr : Set :=
  | Var : nat -> IFExpr
  | Tr : IFExpr
  | Fa : IFExpr
  | IfE : IFExpr -> IFExpr -> IFExpr -> IFExpr.

Type
  (fun F : IFExpr =>
   match F return Prop with
   | IfE (Var _) H I => True
   | IfE _ _ _ => False
   | _ => True
   end).