aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/failure/Case2.v
blob: f8c95b1ecb4c7fb7ca59d55d5177a196cd29aeb6 (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.

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