diff options
Diffstat (limited to 'theories/Init/Datatypes.v')
| -rw-r--r-- | theories/Init/Datatypes.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 0f2717beef..9f77221d5a 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -26,6 +26,8 @@ Inductive Empty_set : Set :=. Inductive unit : Set := tt : unit. +Register unit as core.unit.type. +Register tt as core.unit.tt. (********************************************************************) (** * The boolean datatype *) @@ -198,6 +200,10 @@ Notation "x + y" := (sum x y) : type_scope. Arguments inl {A B} _ , [A] B _. Arguments inr {A B} _ , A [B] _. +Register sum as core.sum.type. +Register inl as core.sum.inl. +Register inr as core.sum.inr. + (** [prod A B], written [A * B], is the product of [A] and [B]; the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *) |