[coqlib] Rebindable Coqlib namespace.

We refactor the `Coqlib` API to locate objects over a namespace
`module.object.property`.

This introduces the vernacular command `Register g as n` to expose the
Coq constant `g` under the name `n` (through the `register_ref`
function). The constant can then be dynamically located using the
`lib_ref` function.

Co-authored-by: Emilio Jesús Gallego Arias <e+git@x80.org>
Co-authored-by: Maxime Dénès <mail@maximedenes.fr>
Co-authored-by: Vincent Laporte <Vincent.Laporte@fondation-inria.fr>

23 files changed, 243 insertions, 0 deletions

diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 6f220f2023..0c68b75124 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -83,6 +83,8 @@ Proof.
   apply le_dec.
 Defined.
 
+Register le_gt_dec as num.nat.le_gt_dec.
+
 (** Proofs of decidability *)
 
 Theorem dec_le n m : decidable (n <= m).
@@ -130,6 +132,16 @@ Proof.
   apply Nat.nlt_ge.
 Qed.
 
+Register dec_le as num.nat.dec_le.
+Register dec_lt as num.nat.dec_lt.
+Register dec_ge as num.nat.dec_ge.
+Register dec_gt as num.nat.dec_gt.
+Register not_eq as num.nat.not_eq.
+Register not_le as num.nat.not_le.
+Register not_lt as num.nat.not_lt.
+Register not_ge as num.nat.not_ge.
+Register not_gt as num.nat.not_gt.
+
 
 (** A ternary comparison function in the spirit of [Z.compare].
     See now [Nat.compare] and its properties.
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index 3bf6cd952f..d6adb7e205 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -46,6 +46,8 @@ Proof.
  symmetry. apply Nat.sub_1_r.
 Qed.
 
+Register pred_of_minus as num.nat.pred_of_minus.
+
 (** * Diagonal *)
 
 Notation minus_diag := Nat.sub_diag (only parsing). (* n - n = 0 *)
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 9a24c804a1..ddbc128aa1 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -30,6 +30,8 @@ Proof.
   elim (Nat.eq_dec n m); [left|right]; trivial.
 Defined.
 
+Register dec_eq_nat as num.nat.eq_dec.
+
 Definition UIP_nat:= Eqdep_dec.UIP_dec Nat.eq_dec.
 
 Import EqNotations.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 8a0265438a..75f14bb4da 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -41,6 +41,10 @@ Declare Scope bool_scope.
 Delimit Scope bool_scope with bool.
 Bind Scope bool_scope with bool.
 
+Register bool as core.bool.type.
+Register true as core.bool.true.
+Register false as core.bool.false.
+
 (** Basic boolean operators *)
 
 Definition andb (b1 b2:bool) : bool := if b1 then b2 else false.
@@ -62,6 +66,11 @@ Definition negb (b:bool) := if b then false else true.
 Infix "||" := orb : bool_scope.
 Infix "&&" := andb : bool_scope.
 
+Register andb as core.bool.andb.
+Register orb as core.bool.orb.
+Register xorb as core.bool.xorb.
+Register negb as core.bool.negb.
+
 (** Basic properties of [andb] *)
 
 Lemma andb_prop : forall a b:bool, andb a b = true -> a = true /\ b = true.
@@ -70,6 +79,8 @@ Proof.
 Qed.
 Hint Resolve andb_prop: bool.
 
+Register andb_prop as core.bool.andb_prop.
+
 Lemma andb_true_intro :
   forall b1 b2:bool, b1 = true /\ b2 = true -> andb b1 b2 = true.
 Proof.
@@ -77,12 +88,16 @@ Proof.
 Qed.
 Hint Resolve andb_true_intro: bool.
 
+Register andb_true_intro as core.bool.andb_true_intro.
+
 (** Interpretation of booleans as propositions *)
 
 Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.
 
 Hint Constructors eq_true : eq_true.
 
+Register eq_true as core.eq_true.type.
+
 (** Another way of interpreting booleans as propositions *)
 
 Definition is_true b := b = true.
@@ -141,6 +156,9 @@ Delimit Scope nat_scope with nat.
 Bind Scope nat_scope with nat.
 Arguments S _%nat.
 
+Register nat as num.nat.type.
+Register O as num.nat.O.
+Register S as num.nat.S.
 
 (********************************************************************)
 (** * Container datatypes *)
@@ -156,6 +174,10 @@ Inductive option (A:Type) : Type :=
 Arguments Some {A} a.
 Arguments None {A}.
 
+Register option as core.option.type.
+Register Some as core.option.Some.
+Register None as core.option.None.
+
 Definition option_map (A B:Type) (f:A->B) (o : option A) : option B :=
   match o with
     | Some a => @Some B (f a)
@@ -187,11 +209,19 @@ Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
 
 Arguments pair {A B} _ _.
 
+Register prod as core.prod.type.
+Register pair as core.prod.intro.
+Register prod_rect as core.prod.rect.
+
 Section projections.
   Context {A : Type} {B : Type}.
 
   Definition fst (p:A * B) := match p with (x, y) => x end.
   Definition snd (p:A * B) := match p with (x, y) => y end.
+
+  Register fst as core.prod.proj1.
+  Register snd as core.prod.proj2.
+
 End projections.
 
 Hint Resolve pair inl inr: core.
@@ -239,6 +269,10 @@ Bind Scope list_scope with list.
 
 Infix "::" := cons (at level 60, right associativity) : list_scope.
 
+Register list as core.list.type.
+Register nil as core.list.nil.
+Register cons as core.list.cons.
+
 Local Open Scope list_scope.
 
 Definition length (A : Type) : list A -> nat :=
@@ -269,6 +303,11 @@ Inductive comparison : Set :=
   | Lt : comparison
   | Gt : comparison.
 
+Register comparison as core.comparison.type.
+Register Eq as core.comparison.Eq.
+Register Lt as core.comparison.Lt.
+Register Gt as core.comparison.Gt.
+
 Lemma comparison_eq_stable : forall c c' : comparison, ~~ c = c' -> c = c'.
 Proof.
   destruct c, c'; intro H; reflexivity || destruct H; discriminate.
@@ -353,6 +392,10 @@ Arguments identity_ind [A] a P f y i.
 Arguments identity_rec [A] a P f y i.
 Arguments identity_rect [A] a P f y i.
 
+Register identity as core.identity.type.
+Register identity_refl as core.identity.refl.
+Register identity_ind as core.identity.ind.
+
 (** Identity type *)
 
 Definition ID := forall A:Type, A -> A.
@@ -361,6 +404,8 @@ Definition id : ID := fun A x => x.
 Definition IDProp := forall A:Prop, A -> A.
 Definition idProp : IDProp := fun A x => x.
 
+Register IDProp as core.IDProp.type.
+Register idProp as core.IDProp.idProp.
 
 (* begin hide *)
 
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 4ec0049a9c..1db0a8e1b5 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -21,14 +21,21 @@ Notation "A -> B" := (forall (_ : A), B) : type_scope.
 Inductive True : Prop :=
   I : True.
 
+Register True as core.True.type.
+Register I as core.True.I.
+
 (** [False] is the always false proposition *)
 Inductive False : Prop :=.
 
+Register False as core.False.type.
+
 (** [not A], written [~A], is the negation of [A] *)
 Definition not (A:Prop) := A -> False.
 
 Notation "~ x" := (not x) : type_scope.
 
+Register not as core.not.type.
+
 (** Create the "core" hint database, and set its transparent state for
   variables and constants explicitely. *)
 
@@ -50,6 +57,9 @@ Inductive and (A B:Prop) : Prop :=
 
 where "A /\ B" := (and A B) : type_scope.
 
+Register and as core.and.type.
+Register conj as core.and.conj.
+
 Section Conjunction.
 
   Variables A B : Prop.
@@ -77,12 +87,18 @@ where "A \/ B" := (or A B) : type_scope.
 Arguments or_introl [A B] _, [A] B _.
 Arguments or_intror [A B] _, A [B] _.
 
+Register or as core.or.type.
+
 (** [iff A B], written [A <-> B], expresses the equivalence of [A] and [B] *)
 
 Definition iff (A B:Prop) := (A -> B) /\ (B -> A).
 
 Notation "A <-> B" := (iff A B) : type_scope.
 
+Register iff as core.iff.type.
+Register proj1 as core.iff.proj1.
+Register proj2 as core.iff.proj2.
+
 Section Equivalence.
 
 Theorem iff_refl : forall A:Prop, A <-> A.
@@ -257,6 +273,8 @@ Notation "'IF' c1 'then' c2 'else' c3" := (IF_then_else c1 c2 c3)
 Inductive ex (A:Type) (P:A -> Prop) : Prop :=
   ex_intro : forall x:A, P x -> ex (A:=A) P.
 
+Register ex as core.ex.type.
+
 Inductive ex2 (A:Type) (P Q:A -> Prop) : Prop :=
   ex_intro2 : forall x:A, P x -> Q x -> ex2 (A:=A) P Q.
 
@@ -333,6 +351,11 @@ Hint Resolve I conj or_introl or_intror : core.
 Hint Resolve eq_refl: core.
 Hint Resolve ex_intro ex_intro2: core.
 
+Register eq as core.eq.type.
+Register eq_refl as core.eq.refl.
+Register eq_ind as core.eq.ind.
+Register eq_rect as core.eq.rect.
+
 Section Logic_lemmas.
 
   Theorem absurd : forall A C:Prop, A -> ~ A -> C.
@@ -351,16 +374,22 @@ Section Logic_lemmas.
       destruct 1; trivial.
     Defined.
 
+    Register eq_sym as core.eq.sym.
+
     Theorem eq_trans : x = y -> y = z -> x = z.
     Proof.
       destruct 2; trivial.
     Defined.
 
+    Register eq_trans as core.eq.trans.
+
     Theorem f_equal : x = y -> f x = f y.
     Proof.
       destruct 1; trivial.
     Defined.
 
+    Register f_equal as core.eq.congr.
+
     Theorem not_eq_sym : x <> y -> y <> x.
     Proof.
       red; intros h1 h2; apply h1; destruct h2; trivial.
@@ -373,6 +402,8 @@ Section Logic_lemmas.
     intros A x P H y H0. elim eq_sym with (1 := H0); assumption.
   Defined.
 
+  Register eq_ind_r as core.eq.ind_r.
+
   Definition eq_rec_r :
     forall (A:Type) (x:A) (P:A -> Set), P x -> forall y:A, y = x -> P y.
     intros A x P H y H0; elim eq_sym with (1 := H0); assumption.
@@ -458,6 +489,8 @@ Proof.
   destruct 1; destruct 1; reflexivity.
 Qed.
 
+Register f_equal2 as core.eq.congr2.
+
 Theorem f_equal3 :
   forall (A1 A2 A3 B:Type) (f:A1 -> A2 -> A3 -> B) (x1 y1:A1)
     (x2 y2:A2) (x3 y3:A3),
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 6f10a93997..587de12a15 100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -51,6 +51,11 @@ Section identity_is_a_congruence.
 
 End identity_is_a_congruence.
 
+Register identity_sym as core.identity.sym.
+Register identity_trans as core.identity.trans.
+Register identity_congr as core.identity.congr.
+
+
 Definition identity_ind_r :
   forall (A:Type) (a:A) (P:A -> Prop), P a -> forall y:A, identity y a -> P y.
  intros A x P H y H0; case identity_sym with (1 := H0); trivial.
diff --git a/theories/Init/Nat.v b/theories/Init/Nat.v
index eb4ba0e5e6..7e7a1ced58 100644
--- a/theories/Init/Nat.v
+++ b/theories/Init/Nat.v
@@ -42,6 +42,8 @@ Definition pred n :=
     | S u => u
   end.
 
+Register pred as num.nat.pred.
+
 Fixpoint add n m :=
   match n with
   | 0 => m
@@ -50,6 +52,8 @@ Fixpoint add n m :=
 
 where "n + m" := (add n m) : nat_scope.
 
+Register add as num.nat.add.
+
 Definition double n := n + n.
 
 Fixpoint mul n m :=
@@ -60,6 +64,8 @@ Fixpoint mul n m :=
 
 where "n * m" := (mul n m) : nat_scope.
 
+Register mul as num.nat.mul.
+
 (** Truncated subtraction: [n-m] is [0] if [n<=m] *)
 
 Fixpoint sub n m :=
@@ -70,6 +76,8 @@ Fixpoint sub n m :=
 
 where "n - m" := (sub n m) : nat_scope.
 
+Register sub as num.nat.sub.
+
 (** ** Comparisons *)
 
 Fixpoint eqb n m : bool :=
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 65e5e76a22..4489f4cb15 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -182,6 +182,11 @@ Notation "x <= y < z" := (x <= y /\ y < z) : nat_scope.
 Notation "x < y < z" := (x < y /\ y < z) : nat_scope.
 Notation "x < y <= z" := (x < y /\ y <= z) : nat_scope.
 
+Register le as num.nat.le.
+Register lt as num.nat.lt.
+Register ge as num.nat.ge.
+Register gt as num.nat.gt.
+
 Theorem le_pred : forall n m, n <= m -> pred n <= pred m.
 Proof.
 induction 1; auto. destruct m; simpl; auto.
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index a5f926f7ab..e4796a8059 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -27,6 +27,10 @@ Require Import Logic.
 Inductive sig (A:Type) (P:A -> Prop) : Type :=
     exist : forall x:A, P x -> sig P.
 
+Register sig as core.sig.type.
+Register exist as core.sig.intro.
+Register sig_rect as core.sig.rect.
+
 Inductive sig2 (A:Type) (P Q:A -> Prop) : Type :=
     exist2 : forall x:A, P x -> Q x -> sig2 P Q.
 
@@ -36,6 +40,10 @@ Inductive sig2 (A:Type) (P Q:A -> Prop) : Type :=
 Inductive sigT (A:Type) (P:A -> Type) : Type :=
     existT : forall x:A, P x -> sigT P.
 
+Register sigT as core.sigT.type.
+Register existT as core.sigT.intro.
+Register sigT_rect as core.sigT.rect.
+
 Inductive sigT2 (A:Type) (P Q:A -> Type) : Type :=
     existT2 : forall x:A, P x -> Q x -> sigT2 P Q.
 
@@ -93,6 +101,9 @@ Section Subset_projections.
     | exist _ a b => b
     end.
 
+  Register proj1_sig as core.sig.proj1.
+  Register proj2_sig as core.sig.proj2.
+
 End Subset_projections.
 
 
@@ -152,6 +163,9 @@ Section Projections.
     | existT _ _ h => h
     end.
 
+  Register projT1 as core.sigT.proj1.
+  Register projT2 as core.sigT.proj2.
+
 End Projections.
 
 Local Notation "( x ; y )" := (existT _ x y) (at level 0, format "( x ;  '/  ' y )").
@@ -681,6 +695,8 @@ Add Printing If sumbool.
 Arguments left {A B} _, [A] B _.
 Arguments right {A B} _ , A [B] _.
 
+Register sumbool as core.sumbool.type.
+
 (** [sumor] is an option type equipped with the justification of why
     it may not be a regular value *)
 
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index c27ffa33f8..f4cb34c713 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -42,6 +42,8 @@ Section Well_founded.
 
  Definition well_founded := forall a:A, Acc a.
 
+ Register well_founded as core.wf.well_founded.
+
  (** Well-founded induction on [Set] and [Prop] *)
 
  Hypothesis Rwf : well_founded.
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.
diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v
index 7b6740e94b..ef2c688759 100644
--- a/theories/Numbers/BinNums.v
+++ b/theories/Numbers/BinNums.v
@@ -29,6 +29,10 @@ Bind Scope positive_scope with positive.
 Arguments xO _%positive.
 Arguments xI _%positive.
 
+Register xI as num.pos.xI.
+Register xO as num.pos.xO.
+Register xH as num.pos.xH.
+
 (** [N] is a datatype representing natural numbers in a binary way,
     by extending the [positive] datatype with a zero.
     Numbers in [N] will also be denoted using a decimal notation;
@@ -43,6 +47,10 @@ Delimit Scope N_scope with N.
 Bind Scope N_scope with N.
 Arguments Npos _%positive.
 
+Register N as num.N.type.
+Register N0 as num.N.N0.
+Register Npos as num.N.Npos.
+
 (** [Z] is a datatype representing the integers in a binary way.
     An integer is either zero or a strictly positive number
     (coded as a [positive]) or a strictly negative number
@@ -60,3 +68,8 @@ Delimit Scope Z_scope with Z.
 Bind Scope Z_scope with Z.
 Arguments Zpos _%positive.
 Arguments Zneg _%positive.
+
+Register Z as num.Z.type.
+Register Z0 as num.Z.Z0.
+Register Zpos as num.Z.Zpos.
+Register Zneg as num.Z.Zneg.
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index edbae6534a..001e1cfb01 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -237,6 +237,8 @@ Tactic Notation "destruct_call" constr(f) "as" simple_intropattern(l) "in" hyp(i
 
 Definition fix_proto {A : Type} (a : A) := a.
 
+Register fix_proto as program.tactic.fix_proto.
+
 Ltac destruct_rec_calls :=
   match goal with
     | [ H : fix_proto _ |- _ ] => destruct_calls H ; clear H
@@ -331,3 +333,5 @@ Ltac program_simpl := program_simplify ; try typeclasses eauto 10 with program ;
 Obligation Tactic := program_simpl.
 
 Definition obligation (A : Type) {a : A} := a.
+
+Register obligation as program.tactics.obligation.
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 6278798543..8479b9a2bb 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -32,6 +32,8 @@ Section Well_founded.
 
   Definition Fix_sub (x : A) := Fix_F_sub x (Rwf x).
 
+  Register Fix_sub as program.wf.fix_sub.
+
   (* Notation Fix_F := (Fix_F_sub P F_sub) (only parsing). (* alias *) *)
   (* Definition Fix (x:A) := Fix_F_sub P F_sub x (Rwf x). *)
 
@@ -89,6 +91,8 @@ Section Measure_well_founded.
 
   Definition MR (x y: T): Prop := R (m x) (m y).
 
+  Register MR as program.wf.mr.
+
   Lemma measure_wf: well_founded MR.
   Proof with auto.
     unfold well_founded.
diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v
index af06bcf47e..43c8d9bc09 100644
--- a/theories/Setoids/Setoid.v
+++ b/theories/Setoids/Setoid.v
@@ -17,6 +17,8 @@ Export Morphisms.ProperNotations.
 Definition Setoid_Theory := @Equivalence.
 Definition Build_Setoid_Theory := @Build_Equivalence.
 
+Register Build_Setoid_Theory as plugins.setoid_ring.Build_Setoid_Theory.
+
 Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x.
 Proof.
   unfold Setoid_Theory in s. intros ; reflexivity.
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index 3f676c1888..d1168694b2 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -20,6 +20,8 @@ Require Import Bool BinPos BinNat PeanoNat Nnat.
 
 Inductive ascii : Set := Ascii (_ _ _ _ _ _ _ _ : bool).
 
+Register Ascii as plugins.syntax.Ascii.
+
 Declare Scope char_scope.
 Declare ML Module "ascii_syntax_plugin".
 Delimit Scope char_scope with char.
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index b27474ef25..f6cc8c99ed 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -30,6 +30,9 @@ Delimit Scope string_scope with string.
 Bind Scope string_scope with string.
 Local Open Scope string_scope.
 
+Register EmptyString as plugins.syntax.EmptyString.
+Register String as plugins.syntax.String.
+
 (** Equality is decidable *)
 
 Definition string_dec : forall s1 s2 : string, {s1 = s2} + {s1 <> s2}.
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 1241345338..8fc3ab56c9 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -38,6 +38,14 @@ Module Z
 
 Include BinIntDef.Z.
 
+Register add as num.Z.add.
+Register opp as num.Z.opp.
+Register succ as num.Z.succ.
+Register pred as num.Z.pred.
+Register sub as num.Z.sub.
+Register mul as num.Z.mul.
+Register of_nat as num.Z.of_nat.
+
 (** When including property functors, only inline t eq zero one two *)
 
 Set Inline Level 30.
@@ -68,6 +76,11 @@ Notation "( x | y )" := (divide x y) (at level 0).
 Definition Even a := exists b, a = 2*b.
 Definition Odd a := exists b, a = 2*b+1.
 
+Register le as num.Z.le.
+Register lt as num.Z.lt.
+Register ge as num.Z.ge.
+Register gt as num.Z.gt.
+
 (** * Decidability of equality. *)
 
 Definition eq_dec (x y : Z) : {x = y} + {x <> y}.
@@ -477,6 +490,10 @@ Qed.
 
 Include ZBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
 
+Register eq_decidable as num.Z.eq_decidable.
+Register le_decidable as num.Z.le_decidable.
+Register lt_decidable as num.Z.lt_decidable.
+
 
 (** ** Specification of absolute value *)
 
@@ -1752,6 +1769,8 @@ weak_Zmult_plus_distr_r (now Z.mul_add_distr_pos)
 
 Definition Zne (x y:Z) := x <> y. (* TODO : to remove someday ? *)
 
+Register Zne as plugins.omega.Zne.
+
 Ltac elim_compare com1 com2 :=
   case (Dcompare (com1 ?= com2)%Z);
     [ idtac | let x := fresh "H" in
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 5c960da1fb..776efa2978 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -609,6 +609,8 @@ Proof.
  destruct n. trivial. simpl. apply Pos2Z.inj_succ.
 Qed.
 
+Register inj_succ as num.Nat2Z.inj_succ.
+
 (** [Z.of_N] produce non-negative integers *)
 
 Lemma is_nonneg n : 0 <= Z.of_nat n.
@@ -676,11 +678,15 @@ Proof.
  now rewrite <- !nat_N_Z, Nat2N.inj_add, N2Z.inj_add.
 Qed.
 
+Register inj_add as num.Nat2Z.inj_add.
+
 Lemma inj_mul n m : Z.of_nat (n*m) = Z.of_nat n * Z.of_nat m.
 Proof.
  now rewrite <- !nat_N_Z, Nat2N.inj_mul, N2Z.inj_mul.
 Qed.
 
+Register inj_mul as num.Nat2Z.inj_mul.
+
 Lemma inj_sub_max n m : Z.of_nat (n-m) = Z.max 0 (Z.of_nat n - Z.of_nat m).
 Proof.
  now rewrite <- !nat_N_Z, Nat2N.inj_sub, N2Z.inj_sub_max.
@@ -692,6 +698,8 @@ Proof.
  now rewrite <- !nat_N_Z, Nat2N.inj_sub, N2Z.inj_sub.
 Qed.
 
+Register inj_sub as num.Nat2Z.inj_sub.
+
 Lemma inj_pred_max n : Z.of_nat (Nat.pred n) = Z.max 0 (Z.pred (Z.of_nat n)).
 Proof.
  now rewrite <- !nat_N_Z, Nat2N.inj_pred, N2Z.inj_pred_max.
@@ -951,6 +959,14 @@ Definition inj_lt n m := proj1 (Nat2Z.inj_lt n m).
 Definition inj_ge n m := proj1 (Nat2Z.inj_ge n m).
 Definition inj_gt n m := proj1 (Nat2Z.inj_gt n m).
 
+Register neq as plugins.omega.neq.
+Register inj_eq as plugins.omega.inj_eq.
+Register inj_neq as plugins.omega.inj_neq.
+Register inj_le as plugins.omega.inj_le.
+Register inj_lt as plugins.omega.inj_lt.
+Register inj_ge as plugins.omega.inj_ge.
+Register inj_gt as plugins.omega.inj_gt.
+
 (** For the others, a Notation is fine *)
 
 Notation inj_0 := Nat2Z.inj_0 (only parsing).
@@ -1017,3 +1033,5 @@ Theorem inj_minus2 : forall n m:nat, (m > n)%nat -> Z.of_nat (n - m) = 0.
 Proof.
  intros. rewrite not_le_minus_0; auto with arith.
 Qed.
+
+Register inj_minus2 as plugins.omega.inj_minus2.
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 208e84aeb7..bd460f77f0 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -64,6 +64,11 @@ Proof.
   apply Z.lt_gt_cases.
 Qed.
 
+Register dec_Zne as plugins.omega.dec_Zne.
+Register dec_Zgt as plugins.omega.dec_Zgt.
+Register dec_Zge as plugins.omega.dec_Zge.
+Register not_Zeq as plugins.omega.not_Zeq.
+
 (** * Relating strict and large orders *)
 
 Notation Zgt_lt := Z.gt_lt (compat "8.7").
@@ -119,6 +124,12 @@ Proof.
   destruct (Z.eq_decidable n m); [assumption|now elim H].
 Qed.
 
+Register Znot_le_gt as plugins.omega.Znot_le_gt.
+Register Znot_lt_ge as plugins.omega.Znot_lt_ge.
+Register Znot_ge_lt as plugins.omega.Znot_ge_lt.
+Register Znot_gt_le as plugins.omega.Znot_gt_le.
+Register not_Zne as plugins.omega.not_Zne.
+
 (** * Equivalence and order properties *)
 
 (** Reflexivity *)
diff --git a/theories/ZArith/auxiliary.v b/theories/ZArith/auxiliary.v
index 306a856381..fd357502d2 100644
--- a/theories/ZArith/auxiliary.v
+++ b/theories/ZArith/auxiliary.v
@@ -94,3 +94,10 @@ Proof.
  now apply Z.add_lt_mono_l.
 Qed.
 
+Register Zegal_left as plugins.omega.Zegal_left.
+Register Zne_left as plugins.omega.Zne_left.
+Register Zlt_left as plugins.omega.Zlt_left.
+Register Zgt_left as plugins.omega.Zgt_left.
+Register Zle_left as plugins.omega.Zle_left.
+Register Zge_left as plugins.omega.Zge_left.
+Register Zmult_le_approx as plugins.omega.Zmult_le_approx.