blob: 344d42083fb84dd6992160b964bdc23c13cf439d (
plain)
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
29
30
|
Primitive int := #int63_type.
Module bad1.
Polymorphic Inductive badcarry1 (A:Type) : Type :=
| C0: A -> badcarry1 A
| C1: A -> badcarry1 A.
Fail Register badcarry1 as kernel.ind_carry.
End bad1.
Module bad2.
Inductive badcarry2 (A:Set) : Set :=
| C0: A -> badcarry2 A
| C1: A -> badcarry2 A.
Fail Register badcarry2 as kernel.ind_carry.
End bad2.
Module bad3.
Inductive badcarry3 : Type -> Type :=
| C0: forall A, A -> badcarry3 A
| C1: forall A, A -> badcarry3 A.
Fail Register badcarry3 as kernel.ind_carry.
End bad3.
|
