1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
|
(* this bug was a proof of False *)
Set Warnings "+no-template-universe".
(* when we require template poly Coq recognizes that it's not allowed *)
Fail #[universes(template)]
Inductive foo@{i} (A:Type@{i}) : Type@{i+1} := bar (X:Type@{i}) : foo A.
(* variants with letin *)
Fail #[universes(template)]
Inductive foo@{i} (T:=Type@{i}:Type@{i+1}) (A:Type@{i}) : Type@{i+1} := bar (X:T) : foo A.
Fail #[universes(template)]
Record foo@{i} (T:=Type@{i}:Type@{i+1}) (A:Type@{i}) : Type@{i+1} := bar { X:T }.
(* no implicit template poly, no explicit universe annotations *)
Inductive foo (A:Type) := bar X : foo X -> foo A | nonempty.
Arguments nonempty {_}.
Fail Check foo nat : Type@{foo.u0}.
(* template poly didn't activate *)
Definition U := Type.
Definition A : U := foo nat.
Fail Definition down : U -> A := fun u => bar nat u nonempty.
(* this is the one where it's important that it fails *)
|
