Merge PR #10609: Register (for Coqlib.ref_lib) several base datatypes of stdlib

Reviewed-by: JasonGross

1 files changed, 15 insertions, 0 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 9f77221d5a..b094f81dc6 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -21,6 +21,8 @@ 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 :=
@@ -141,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 *)
@@ -370,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. *)
@@ -380,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.