Merge PR #186: [RFC] Coqlib cleanup

3 files changed, 30 insertions, 0 deletions

diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v
index 35920d9134..49276f904f 100644
--- a/theories/Logic/Decidable.v
+++ b/theories/Logic/Decidable.v
@@ -87,6 +87,21 @@ Proof.
 unfold decidable; tauto.
 Qed.
 
+Register dec_True as core.dec.True.
+Register dec_False as core.dec.False.
+Register dec_or as core.dec.or.
+Register dec_and as core.dec.and.
+Register dec_not as core.dec.not.
+Register dec_imp as core.dec.imp.
+Register dec_iff as core.dec.iff.
+Register dec_not_not as core.dec.not_not.
+Register not_not as core.dec.dec_not_not.
+Register not_or as core.dec.not_or.
+Register not_and as core.dec.not_and.
+Register not_imp as core.dec.not_imp.
+Register imp_simp as core.dec.imp_simp.
+Register not_iff as core.dec.not_iff.
+
 (** Results formulated with iff, used in FSetDecide.
     Negation are expanded since it is unclear whether setoid rewrite
     will always perform conversion. *)
diff --git a/theories/Logic/Eqdep_dec.v b/theories/Logic/Eqdep_dec.v
index 0560d9ed46..4e8b48af9f 100644
--- a/theories/Logic/Eqdep_dec.v
+++ b/theories/Logic/Eqdep_dec.v
@@ -347,6 +347,8 @@ Proof.
   apply eq_dec.
 Qed.
 
+Register inj_pair2_eq_dec as core.eqdep_dec.inj_pair2.
+
   (** Examples of short direct proofs of unicity of reflexivity proofs
       on specific domains *)
 
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 9c56b60aa4..25b7811417 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -28,10 +28,15 @@ Set Elimination Schemes.
 
 Arguments JMeq_refl {A x} , [A] x.
 
+Register JMeq as core.JMeq.type.
+Register JMeq_refl as core.JMeq.refl.
+
 Hint Resolve JMeq_refl.
 
 Definition JMeq_hom {A : Type} (x y : A) := JMeq x y.
 
+Register JMeq_hom as core.JMeq.hom.
+
 Lemma JMeq_sym : forall (A B:Type) (x:A) (y:B), JMeq x y -> JMeq y x.
 Proof. 
 intros; destruct H; trivial.
@@ -39,12 +44,16 @@ Qed.
 
 Hint Immediate JMeq_sym.
 
+Register JMeq_sym as core.JMeq.sym.
+
 Lemma JMeq_trans :
  forall (A B C:Type) (x:A) (y:B) (z:C), JMeq x y -> JMeq y z -> JMeq x z.
 Proof.
 destruct 2; trivial.
 Qed.
 
+Register JMeq_trans as core.JMeq.trans.
+
 Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y.
 
 Lemma JMeq_ind : forall (A:Type) (x:A) (P:A -> Prop),
@@ -53,6 +62,8 @@ Proof.
 intros A x P H y H'; case JMeq_eq with (1 := H'); trivial.
 Qed.
 
+Register JMeq_ind as core.JMeq.ind.
+
 Lemma JMeq_rec : forall (A:Type) (x:A) (P:A -> Set),
   P x -> forall y, JMeq x y -> P y.
 Proof.
@@ -89,6 +100,8 @@ Proof.
 intros A x B f y H; case JMeq_eq with (1 := H); trivial.
 Qed.
 
+Register JMeq_congr as core.JMeq.congr.
+
 (** [JMeq] is equivalent to [eq_dep Type (fun X => X)] *)
 
 Require Import Eqdep.