blob: ff99f2e23ca755a865e1559b122befd5c6bd3509 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
(* Unification error tests *)
Module A.
(* Check regression of an UNBOUND_REL bug *)
Inductive T := C : forall {A}, A -> T.
Fail Check fun x => match x return ?[X] with C a => a end.
(* Bug #3634 *)
Fail Check (id:Type -> _).
End A.
|
