blob: 93ba6f17e0d01ed6a53f9f6090b034beedaf6f8d (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
(* Was raising an anomaly before 8.13 *)
Check let 'tt := tt in
let X := nat in
let b : bool := _ in
(fun n : nat => 0 : X) : _.
(* Was raising an ill-typed instance error before 8.13 *)
Check let 'tt := tt in
let X := nat in
let b : bool := true in
(fun n : nat => 0 : X) : _.
|
