test-suite/bugs/closed/shouldsucceed/2300.v


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.