blob: 4e587cbb25f466349508aae5a4dc2ec6faed6e96 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
(* Check some behavior of Ltac pattern-matching wrt universe levels *)
Section contents.
Variables (A: Type) (B: (unit -> Type) -> Type).
Inductive C := c: A -> unit -> C.
Let unused2 (x: unit) := C.
Goal True.
intuition.
Qed.
End contents.
|