aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/bugs/closed/2299.v
blob: c0552ca7b3db5ecbb3165ef287422260531ed127 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
(* Check that destruct refreshes universes in what it generalizes *)

Section test.

Variable A: Type.

Inductive T: unit -> Type := C: A -> unit -> T tt.

Let unused := T tt.

Goal T tt -> False.
 intro X.
 destruct X.