diff options
Diffstat (limited to 'theories/Init')
| -rw-r--r-- | theories/Init/Datatypes.v | 21 | ||||
| -rw-r--r-- | theories/Init/Decimal.v | 2 |
2 files changed, 22 insertions, 1 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 0f2717beef..b094f81dc6 100644 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -21,11 +21,15 @@ Require Import Logic. Inductive Empty_set : Set :=. +Register Empty_set as core.Empty_set.type. + (** [unit] is a singleton datatype with sole inhabitant [tt] *) Inductive unit : Set := tt : unit. +Register unit as core.unit.type. +Register tt as core.unit.tt. (********************************************************************) (** * The boolean datatype *) @@ -139,6 +143,9 @@ Inductive BoolSpec (P Q : Prop) : bool -> Prop := | BoolSpecF : Q -> BoolSpec P Q false. Hint Constructors BoolSpec : core. +Register BoolSpec as core.BoolSpec.type. +Register BoolSpecT as core.BoolSpec.BoolSpecT. +Register BoolSpecF as core.BoolSpec.BoolSpecF. (********************************************************************) (** * Peano natural numbers *) @@ -198,6 +205,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)] *) @@ -364,6 +375,11 @@ Inductive CompareSpec (Peq Plt Pgt : Prop) : comparison -> Prop := | CompGt : Pgt -> CompareSpec Peq Plt Pgt Gt. Hint Constructors CompareSpec : core. +Register CompareSpec as core.CompareSpec.type. +Register CompEq as core.CompareSpec.CompEq. +Register CompLt as core.CompareSpec.CompLt. +Register CompGt as core.CompareSpec.CompGt. + (** For having clean interfaces after extraction, [CompareSpec] is declared in Prop. For some situations, it is nonetheless useful to have a version in Type. Interestingly, these two versions are equivalent. *) @@ -374,6 +390,11 @@ Inductive CompareSpecT (Peq Plt Pgt : Prop) : comparison -> Type := | CompGtT : Pgt -> CompareSpecT Peq Plt Pgt Gt. Hint Constructors CompareSpecT : core. +Register CompareSpecT as core.CompareSpecT.type. +Register CompEqT as core.CompareSpecT.CompEqT. +Register CompLtT as core.CompareSpecT.CompLtT. +Register CompGtT as core.CompareSpecT.CompGtT. + Lemma CompareSpec2Type : forall Peq Plt Pgt c, CompareSpec Peq Plt Pgt c -> CompareSpecT Peq Plt Pgt c. Proof. diff --git a/theories/Init/Decimal.v b/theories/Init/Decimal.v index 855db8bc3f..2a84456500 100644 --- a/theories/Init/Decimal.v +++ b/theories/Init/Decimal.v @@ -179,7 +179,7 @@ Definition del_head_int n d := (** [del_tail n d] removes [n] digits at end of [d] or returns [zero] if [d] has less than [n] digits. *) -Fixpoint del_tail n d := rev (del_head n (rev d)). +Definition del_tail n d := rev (del_head n (rev d)). Definition del_tail_int n d := match d with |