diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 7e4c4ce5c69d..ee2c87d19ad6 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -127,250 +127,143 @@ let selecti s m =
       * MODULE END: M
       *)
 module M = struct
-  (**
-    * Location of the Coq libraries.
-    *)
-
-  let logic_dir = ["Coq"; "Logic"; "Decidable"]
-
-  let mic_modules =
-    [ ["Coq"; "Lists"; "List"]
-    ; ["Coq"; "micromega"; "ZMicromega"]
-    ; ["Coq"; "micromega"; "Tauto"]
-    ; ["Coq"; "micromega"; "DeclConstant"]
-    ; ["Coq"; "micromega"; "RingMicromega"]
-    ; ["Coq"; "micromega"; "EnvRing"]
-    ; ["Coq"; "micromega"; "ZMicromega"]
-    ; ["Coq"; "micromega"; "RMicromega"]
-    ; ["Coq"; "micromega"; "Tauto"]
-    ; ["Coq"; "micromega"; "RingMicromega"]
-    ; ["Coq"; "micromega"; "EnvRing"]
-    ; ["Coq"; "QArith"; "QArith_base"]
-    ; ["Coq"; "Reals"; "Rdefinitions"]
-    ; ["Coq"; "Reals"; "Rpow_def"]
-    ; ["LRing_normalise"] ]
-
-  [@@@ocaml.warning "-3"]
-
-  let coq_modules =
-    Coqlib.(
-      init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules
-      @ mic_modules)
-
-  let bin_module = [["Coq"; "Numbers"; "BinNums"]]
-
-  let r_modules =
-    [ ["Coq"; "Reals"; "Rdefinitions"]
-    ; ["Coq"; "Reals"; "Rpow_def"]
-    ; ["Coq"; "Reals"; "Raxioms"]
-    ; ["Coq"; "QArith"; "Qreals"] ]
-
-  let z_modules = [["Coq"; "ZArith"; "BinInt"]]
-
   (**
     * Initialization : a large amount of Caml symbols are derived from
     * ZMicromega.v
     *)
 
-  let gen_constant_in_modules s m n =
+  let constr_of_ref str =
     EConstr.of_constr
-      ( UnivGen.constr_of_monomorphic_global
-      @@ Coqlib.gen_reference_in_modules s m n )
-
-  let init_constant = gen_constant_in_modules "ZMicromega" Coqlib.init_modules
-
-  [@@@ocaml.warning "+3"]
-
-  let constant = gen_constant_in_modules "ZMicromega" coq_modules
-  let bin_constant = gen_constant_in_modules "ZMicromega" bin_module
-  let r_constant = gen_constant_in_modules "ZMicromega" r_modules
-  let z_constant = gen_constant_in_modules "ZMicromega" z_modules
-  let m_constant = gen_constant_in_modules "ZMicromega" mic_modules
-  let coq_and = lazy (init_constant "and")
-  let coq_or = lazy (init_constant "or")
-  let coq_not = lazy (init_constant "not")
-  let coq_iff = lazy (init_constant "iff")
-  let coq_True = lazy (init_constant "True")
-  let coq_False = lazy (init_constant "False")
-  let coq_cons = lazy (constant "cons")
-  let coq_nil = lazy (constant "nil")
-  let coq_list = lazy (constant "list")
-  let coq_O = lazy (init_constant "O")
-  let coq_S = lazy (init_constant "S")
-  let coq_nat = lazy (init_constant "nat")
-  let coq_unit = lazy (init_constant "unit")
+      (UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref str))
+
+  let coq_and = lazy (constr_of_ref "core.and.type")
+  let coq_or = lazy (constr_of_ref "core.or.type")
+  let coq_not = lazy (constr_of_ref "core.not.type")
+  let coq_iff = lazy (constr_of_ref "core.iff.type")
+  let coq_True = lazy (constr_of_ref "core.True.type")
+  let coq_False = lazy (constr_of_ref "core.False.type")
+  let coq_cons = lazy (constr_of_ref "core.list.cons")
+  let coq_nil = lazy (constr_of_ref "core.list.nil")
+  let coq_list = lazy (constr_of_ref "core.list.type")
+  let coq_O = lazy (constr_of_ref "num.nat.O")
+  let coq_S = lazy (constr_of_ref "num.nat.S")
+  let coq_nat = lazy (constr_of_ref "num.nat.type")
+  let coq_unit = lazy (constr_of_ref "core.unit.type")
 
   (*  let coq_option = lazy (init_constant "option")*)
-  let coq_None = lazy (init_constant "None")
-  let coq_tt = lazy (init_constant "tt")
-  let coq_Inl = lazy (init_constant "inl")
-  let coq_Inr = lazy (init_constant "inr")
-  let coq_N0 = lazy (bin_constant "N0")
-  let coq_Npos = lazy (bin_constant "Npos")
-  let coq_xH = lazy (bin_constant "xH")
-  let coq_xO = lazy (bin_constant "xO")
-  let coq_xI = lazy (bin_constant "xI")
-  let coq_Z = lazy (bin_constant "Z")
-  let coq_ZERO = lazy (bin_constant "Z0")
-  let coq_POS = lazy (bin_constant "Zpos")
-  let coq_NEG = lazy (bin_constant "Zneg")
-  let coq_Q = lazy (constant "Q")
-  let coq_R = lazy (constant "R")
-  let coq_Qmake = lazy (constant "Qmake")
-  let coq_Rcst = lazy (constant "Rcst")
-  let coq_C0 = lazy (m_constant "C0")
-  let coq_C1 = lazy (m_constant "C1")
-  let coq_CQ = lazy (m_constant "CQ")
-  let coq_CZ = lazy (m_constant "CZ")
-  let coq_CPlus = lazy (m_constant "CPlus")
-  let coq_CMinus = lazy (m_constant "CMinus")
-  let coq_CMult = lazy (m_constant "CMult")
-  let coq_CPow = lazy (m_constant "CPow")
-  let coq_CInv = lazy (m_constant "CInv")
-  let coq_COpp = lazy (m_constant "COpp")
-  let coq_R0 = lazy (constant "R0")
-  let coq_R1 = lazy (constant "R1")
-  let coq_proofTerm = lazy (constant "ZArithProof")
-  let coq_doneProof = lazy (constant "DoneProof")
-  let coq_ratProof = lazy (constant "RatProof")
-  let coq_cutProof = lazy (constant "CutProof")
-  let coq_enumProof = lazy (constant "EnumProof")
-  let coq_ExProof = lazy (constant "ExProof")
-  let coq_Zgt = lazy (z_constant "Z.gt")
-  let coq_Zge = lazy (z_constant "Z.ge")
-  let coq_Zle = lazy (z_constant "Z.le")
-  let coq_Zlt = lazy (z_constant "Z.lt")
-  let coq_Eq = lazy (init_constant "eq")
-  let coq_Zplus = lazy (z_constant "Z.add")
-  let coq_Zminus = lazy (z_constant "Z.sub")
-  let coq_Zopp = lazy (z_constant "Z.opp")
-  let coq_Zmult = lazy (z_constant "Z.mul")
-  let coq_Zpower = lazy (z_constant "Z.pow")
-  let coq_Qle = lazy (constant "Qle")
-  let coq_Qlt = lazy (constant "Qlt")
-  let coq_Qeq = lazy (constant "Qeq")
-  let coq_Qplus = lazy (constant "Qplus")
-  let coq_Qminus = lazy (constant "Qminus")
-  let coq_Qopp = lazy (constant "Qopp")
-  let coq_Qmult = lazy (constant "Qmult")
-  let coq_Qpower = lazy (constant "Qpower")
-  let coq_Rgt = lazy (r_constant "Rgt")
-  let coq_Rge = lazy (r_constant "Rge")
-  let coq_Rle = lazy (r_constant "Rle")
-  let coq_Rlt = lazy (r_constant "Rlt")
-  let coq_Rplus = lazy (r_constant "Rplus")
-  let coq_Rminus = lazy (r_constant "Rminus")
-  let coq_Ropp = lazy (r_constant "Ropp")
-  let coq_Rmult = lazy (r_constant "Rmult")
-  let coq_Rinv = lazy (r_constant "Rinv")
-  let coq_Rpower = lazy (r_constant "pow")
-  let coq_powerZR = lazy (r_constant "powerRZ")
-  let coq_IZR = lazy (r_constant "IZR")
-  let coq_IQR = lazy (r_constant "Q2R")
-  let coq_PEX = lazy (constant "PEX")
-  let coq_PEc = lazy (constant "PEc")
-  let coq_PEadd = lazy (constant "PEadd")
-  let coq_PEopp = lazy (constant "PEopp")
-  let coq_PEmul = lazy (constant "PEmul")
-  let coq_PEsub = lazy (constant "PEsub")
-  let coq_PEpow = lazy (constant "PEpow")
-  let coq_PX = lazy (constant "PX")
-  let coq_Pc = lazy (constant "Pc")
-  let coq_Pinj = lazy (constant "Pinj")
-  let coq_OpEq = lazy (constant "OpEq")
-  let coq_OpNEq = lazy (constant "OpNEq")
-  let coq_OpLe = lazy (constant "OpLe")
-  let coq_OpLt = lazy (constant "OpLt")
-  let coq_OpGe = lazy (constant "OpGe")
-  let coq_OpGt = lazy (constant "OpGt")
-  let coq_PsatzIn = lazy (constant "PsatzIn")
-  let coq_PsatzSquare = lazy (constant "PsatzSquare")
-  let coq_PsatzMulE = lazy (constant "PsatzMulE")
-  let coq_PsatzMultC = lazy (constant "PsatzMulC")
-  let coq_PsatzAdd = lazy (constant "PsatzAdd")
-  let coq_PsatzC = lazy (constant "PsatzC")
-  let coq_PsatzZ = lazy (constant "PsatzZ")
+  let coq_None = lazy (constr_of_ref "core.option.None")
+  let coq_tt = lazy (constr_of_ref "core.unit.tt")
+  let coq_Inl = lazy (constr_of_ref "core.sum.inl")
+  let coq_Inr = lazy (constr_of_ref "core.sum.inr")
+  let coq_N0 = lazy (constr_of_ref "num.N.N0")
+  let coq_Npos = lazy (constr_of_ref "num.N.Npos")
+  let coq_xH = lazy (constr_of_ref "num.pos.xH")
+  let coq_xO = lazy (constr_of_ref "num.pos.xO")
+  let coq_xI = lazy (constr_of_ref "num.pos.xI")
+  let coq_Z = lazy (constr_of_ref "num.Z.type")
+  let coq_ZERO = lazy (constr_of_ref "num.Z.Z0")
+  let coq_POS = lazy (constr_of_ref "num.Z.Zpos")
+  let coq_NEG = lazy (constr_of_ref "num.Z.Zneg")
+  let coq_Q = lazy (constr_of_ref "rat.Q.type")
+  let coq_Qmake = lazy (constr_of_ref "rat.Q.Qmake")
+  let coq_R = lazy (constr_of_ref "reals.R.type")
+  let coq_Rcst = lazy (constr_of_ref "micromega.Rcst.type")
+  let coq_C0 = lazy (constr_of_ref "micromega.Rcst.C0")
+  let coq_C1 = lazy (constr_of_ref "micromega.Rcst.C1")
+  let coq_CQ = lazy (constr_of_ref "micromega.Rcst.CQ")
+  let coq_CZ = lazy (constr_of_ref "micromega.Rcst.CZ")
+  let coq_CPlus = lazy (constr_of_ref "micromega.Rcst.CPlus")
+  let coq_CMinus = lazy (constr_of_ref "micromega.Rcst.CMinus")
+  let coq_CMult = lazy (constr_of_ref "micromega.Rcst.CMult")
+  let coq_CPow = lazy (constr_of_ref "micromega.Rcst.CPow")
+  let coq_CInv = lazy (constr_of_ref "micromega.Rcst.CInv")
+  let coq_COpp = lazy (constr_of_ref "micromega.Rcst.COpp")
+  let coq_R0 = lazy (constr_of_ref "reals.R.R0")
+  let coq_R1 = lazy (constr_of_ref "reals.R.R1")
+  let coq_proofTerm = lazy (constr_of_ref "micromega.ZArithProof.type")
+  let coq_doneProof = lazy (constr_of_ref "micromega.ZArithProof.DoneProof")
+  let coq_ratProof = lazy (constr_of_ref "micromega.ZArithProof.RatProof")
+  let coq_cutProof = lazy (constr_of_ref "micromega.ZArithProof.CutProof")
+  let coq_enumProof = lazy (constr_of_ref "micromega.ZArithProof.EnumProof")
+  let coq_ExProof = lazy (constr_of_ref "micromega.ZArithProof.ExProof")
+  let coq_Zgt = lazy (constr_of_ref "num.Z.gt")
+  let coq_Zge = lazy (constr_of_ref "num.Z.ge")
+  let coq_Zle = lazy (constr_of_ref "num.Z.le")
+  let coq_Zlt = lazy (constr_of_ref "num.Z.lt")
+  let coq_Eq = lazy (constr_of_ref "core.eq.type")
+  let coq_Zplus = lazy (constr_of_ref "num.Z.add")
+  let coq_Zminus = lazy (constr_of_ref "num.Z.sub")
+  let coq_Zopp = lazy (constr_of_ref "num.Z.opp")
+  let coq_Zmult = lazy (constr_of_ref "num.Z.mul")
+  let coq_Zpower = lazy (constr_of_ref "num.Z.pow")
+  let coq_Qle = lazy (constr_of_ref "rat.Q.Qle")
+  let coq_Qlt = lazy (constr_of_ref "rat.Q.Qlt")
+  let coq_Qeq = lazy (constr_of_ref "rat.Q.Qeq")
+  let coq_Qplus = lazy (constr_of_ref "rat.Q.Qplus")
+  let coq_Qminus = lazy (constr_of_ref "rat.Q.Qminus")
+  let coq_Qopp = lazy (constr_of_ref "rat.Q.Qopp")
+  let coq_Qmult = lazy (constr_of_ref "rat.Q.Qmult")
+  let coq_Qpower = lazy (constr_of_ref "rat.Q.Qpower")
+  let coq_Rgt = lazy (constr_of_ref "reals.R.Rgt")
+  let coq_Rge = lazy (constr_of_ref "reals.R.Rge")
+  let coq_Rle = lazy (constr_of_ref "reals.R.Rle")
+  let coq_Rlt = lazy (constr_of_ref "reals.R.Rlt")
+  let coq_Rplus = lazy (constr_of_ref "reals.R.Rplus")
+  let coq_Rminus = lazy (constr_of_ref "reals.R.Rminus")
+  let coq_Ropp = lazy (constr_of_ref "reals.R.Ropp")
+  let coq_Rmult = lazy (constr_of_ref "reals.R.Rmult")
+  let coq_Rinv = lazy (constr_of_ref "reals.R.Rinv")
+  let coq_Rpower = lazy (constr_of_ref "reals.R.pow")
+  let coq_powerZR = lazy (constr_of_ref "reals.R.powerRZ")
+  let coq_IZR = lazy (constr_of_ref "reals.R.IZR")
+  let coq_IQR = lazy (constr_of_ref "reals.R.Q2R")
+  let coq_PEX = lazy (constr_of_ref "micromega.PExpr.PEX")
+  let coq_PEc = lazy (constr_of_ref "micromega.PExpr.PEc")
+  let coq_PEadd = lazy (constr_of_ref "micromega.PExpr.PEadd")
+  let coq_PEopp = lazy (constr_of_ref "micromega.PExpr.PEopp")
+  let coq_PEmul = lazy (constr_of_ref "micromega.PExpr.PEmul")
+  let coq_PEsub = lazy (constr_of_ref "micromega.PExpr.PEsub")
+  let coq_PEpow = lazy (constr_of_ref "micromega.PExpr.PEpow")
+  let coq_PX = lazy (constr_of_ref "micromega.Pol.PX")
+  let coq_Pc = lazy (constr_of_ref "micromega.Pol.Pc")
+  let coq_Pinj = lazy (constr_of_ref "micromega.Pol.Pinj")
+  let coq_OpEq = lazy (constr_of_ref "micromega.Op2.OpEq")
+  let coq_OpNEq = lazy (constr_of_ref "micromega.Op2.OpNEq")
+  let coq_OpLe = lazy (constr_of_ref "micromega.Op2.OpLe")
+  let coq_OpLt = lazy (constr_of_ref "micromega.Op2.OpLt")
+  let coq_OpGe = lazy (constr_of_ref "micromega.Op2.OpGe")
+  let coq_OpGt = lazy (constr_of_ref "micromega.Op2.OpGt")
+  let coq_PsatzIn = lazy (constr_of_ref "micromega.Psatz.PsatzIn")
+  let coq_PsatzSquare = lazy (constr_of_ref "micromega.Psatz.PsatzSquare")
+  let coq_PsatzMulE = lazy (constr_of_ref "micromega.Psatz.PsatzMulE")
+  let coq_PsatzMultC = lazy (constr_of_ref "micromega.Psatz.PsatzMulC")
+  let coq_PsatzAdd = lazy (constr_of_ref "micromega.Psatz.PsatzAdd")
+  let coq_PsatzC = lazy (constr_of_ref "micromega.Psatz.PsatzC")
+  let coq_PsatzZ = lazy (constr_of_ref "micromega.Psatz.PsatzZ")
 
   (*  let coq_GT     = lazy (m_constant "GT")*)
 
-  let coq_DeclaredConstant = lazy (m_constant "DeclaredConstant")
-
-  let coq_TT =
-    lazy
-      (gen_constant_in_modules "ZMicromega"
-         [["Coq"; "micromega"; "Tauto"]; ["Tauto"]]
-         "TT")
-
-  let coq_FF =
-    lazy
-      (gen_constant_in_modules "ZMicromega"
-         [["Coq"; "micromega"; "Tauto"]; ["Tauto"]]
-         "FF")
-
-  let coq_And =
-    lazy
-      (gen_constant_in_modules "ZMicromega"
-         [["Coq"; "micromega"; "Tauto"]; ["Tauto"]]
-         "Cj")
+  let coq_DeclaredConstant =
+    lazy (constr_of_ref "micromega.DeclaredConstant.type")
 
-  let coq_Or =
-    lazy
-      (gen_constant_in_modules "ZMicromega"
-         [["Coq"; "micromega"; "Tauto"]; ["Tauto"]]
-         "D")
-
-  let coq_Neg =
-    lazy
-      (gen_constant_in_modules "ZMicromega"
-         [["Coq"; "micromega"; "Tauto"]; ["Tauto"]]
-         "N")
-
-  let coq_Atom =
-    lazy
-      (gen_constant_in_modules "ZMicromega"
-         [["Coq"; "micromega"; "Tauto"]; ["Tauto"]]
-         "A")
-
-  let coq_X =
-    lazy
-      (gen_constant_in_modules "ZMicromega"
-         [["Coq"; "micromega"; "Tauto"]; ["Tauto"]]
-         "X")
-
-  let coq_Impl =
-    lazy
-      (gen_constant_in_modules "ZMicromega"
-         [["Coq"; "micromega"; "Tauto"]; ["Tauto"]]
-         "I")
-
-  let coq_Formula =
-    lazy
-      (gen_constant_in_modules "ZMicromega"
-         [["Coq"; "micromega"; "Tauto"]; ["Tauto"]]
-         "BFormula")
+  let coq_TT = lazy (constr_of_ref "micromega.GFormula.TT")
+  let coq_FF = lazy (constr_of_ref "micromega.GFormula.FF")
+  let coq_And = lazy (constr_of_ref "micromega.GFormula.Cj")
+  let coq_Or = lazy (constr_of_ref "micromega.GFormula.D")
+  let coq_Neg = lazy (constr_of_ref "micromega.GFormula.N")
+  let coq_Atom = lazy (constr_of_ref "micromega.GFormula.A")
+  let coq_X = lazy (constr_of_ref "micromega.GFormula.X")
+  let coq_Impl = lazy (constr_of_ref "micromega.GFormula.I")
+  let coq_Formula = lazy (constr_of_ref "micromega.BFormula.type")
 
   (**
     * Initialization : a few Caml symbols are derived from other libraries;
     * QMicromega, ZArithRing, RingMicromega.
     *)
 
-  let coq_QWitness =
-    lazy
-      (gen_constant_in_modules "QMicromega"
-         [["Coq"; "micromega"; "QMicromega"]]
-         "QWitness")
-
-  let coq_Build =
-    lazy
-      (gen_constant_in_modules "RingMicromega"
-         [["Coq"; "micromega"; "RingMicromega"]; ["RingMicromega"]]
-         "Build_Formula")
-
-  let coq_Cstr =
-    lazy
-      (gen_constant_in_modules "RingMicromega"
-         [["Coq"; "micromega"; "RingMicromega"]; ["RingMicromega"]]
-         "Formula")
+  let coq_QWitness = lazy (constr_of_ref "micromega.QWitness.type")
+  let coq_Build = lazy (constr_of_ref "micromega.Formula.Build_Formula")
+  let coq_Cstr = lazy (constr_of_ref "micromega.Formula.type")
 
   (**
     * Parsing and dumping : transformation functions between Caml and Coq
@@ -1318,29 +1211,10 @@ end
 
 open M
 
-let coq_Branch =
-  lazy
-    (gen_constant_in_modules "VarMap"
-       [["Coq"; "micromega"; "VarMap"]; ["VarMap"]]
-       "Branch")
-
-let coq_Elt =
-  lazy
-    (gen_constant_in_modules "VarMap"
-       [["Coq"; "micromega"; "VarMap"]; ["VarMap"]]
-       "Elt")
-
-let coq_Empty =
-  lazy
-    (gen_constant_in_modules "VarMap"
-       [["Coq"; "micromega"; "VarMap"]; ["VarMap"]]
-       "Empty")
-
-let coq_VarMap =
-  lazy
-    (gen_constant_in_modules "VarMap"
-       [["Coq"; "micromega"; "VarMap"]; ["VarMap"]]
-       "t")
+let coq_Branch = lazy (constr_of_ref "micromega.VarMap.Branch")
+let coq_Elt = lazy (constr_of_ref "micromega.VarMap.Elt")
+let coq_Empty = lazy (constr_of_ref "micromega.VarMap.Empty")
+let coq_VarMap = lazy (constr_of_ref "micromega.VarMap.type")
 
 let rec dump_varmap typ m =
   match m with
@@ -1900,13 +1774,7 @@ let micromega_order_changer cert env ff =
                [ ( "__ff"
                  , ff
                  , EConstr.mkApp (Lazy.force coq_Formula, [|formula_typ|]) )
-               ; ( "__varmap"
-                 , vm
-                 , EConstr.mkApp
-                     ( gen_constant_in_modules "VarMap"
-                         [["Coq"; "micromega"; "VarMap"]; ["VarMap"]]
-                         "t"
-                     , [|typ|] ) )
+               ; ("__varmap", vm, EConstr.mkApp (Lazy.force coq_VarMap, [|typ|]))
                ; ("__wit", cert, cert_typ) ]
                (Tacmach.New.pf_concl gl))
           (*      Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)*)
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 0f2717beef57..9f77221d5aa1 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)] *)
 
diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index bd5225d9ef53..74cdd1797cf4 100644
--- a/theories/QArith/QArith_base.v
+++ b/theories/QArith/QArith_base.v
@@ -22,6 +22,10 @@ Declare Scope Q_scope.
 Delimit Scope Q_scope with Q.
 Bind Scope Q_scope with Q.
 Arguments Qmake _%Z _%positive.
+
+Register Q as rat.Q.type.
+Register Qmake as rat.Q.Qmake.
+
 Open Scope Q_scope.
 Ltac simpl_mult := rewrite ?Pos2Z.inj_mul.
 
@@ -101,6 +105,10 @@ Notation "x > y" := (Qlt y x)(only parsing) : Q_scope.
 Notation "x >= y" := (Qle y x)(only parsing) : Q_scope.
 Notation "x <= y <= z" := (x<=y/\y<=z) : Q_scope.
 
+Register Qeq as rat.Q.Qeq.
+Register Qle as rat.Q.Qle.
+Register Qlt as rat.Q.Qlt.
+
 (** injection from Z is injective. *)
 
 Lemma inject_Z_injective (a b: Z): inject_Z a == inject_Z b <-> a = b.
@@ -278,6 +286,11 @@ Infix "*" := Qmult : Q_scope.
 Notation "/ x" := (Qinv x) : Q_scope.
 Infix "/" := Qdiv : Q_scope.
 
+Register Qplus  as rat.Q.Qplus.
+Register Qminus as rat.Q.Qminus.
+Register Qopp   as rat.Q.Qopp.
+Register Qmult  as rat.Q.Qmult.
+
 (** A light notation for [Zpos] *)
 
 Lemma Qmake_Qdiv a b : a#b==inject_Z a/inject_Z (Zpos b).
@@ -1053,6 +1066,8 @@ Definition Qpower (q:Q) (z:Z) :=
 
 Notation " q ^ z " := (Qpower q z) : Q_scope.
 
+Register Qpower as  rat.Q.Qpower.
+
 Instance Qpower_comp : Proper (Qeq==>eq==>Qeq) Qpower.
 Proof.
 intros x x' Hx y y' Hy. rewrite <- Hy; clear y' Hy.
diff --git a/theories/Reals/Rregisternames.v b/theories/Reals/Rregisternames.v
index f09edef60059..8b078f2cf385 100644
--- a/theories/Reals/Rregisternames.v
+++ b/theories/Reals/Rregisternames.v
@@ -8,7 +8,7 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-Require Import Reals.
+Require Import Raxioms Rfunctions Qreals.
 
 (*****************************************************************)
 (**           Register names for use in plugins                  *)
@@ -18,6 +18,9 @@ Register R as reals.R.type.
 Register R0 as reals.R.R0.
 Register R1 as reals.R.R1.
 Register Rle as reals.R.Rle.
+Register Rgt as reals.R.Rgt.
+Register Rlt as reals.R.Rlt.
+Register Rge as reals.R.Rge.
 Register Rplus as reals.R.Rplus.
 Register Ropp as reals.R.Ropp.
 Register Rminus as reals.R.Rminus.
@@ -26,5 +29,6 @@ Register Rinv as reals.R.Rinv.
 Register Rdiv as reals.R.Rdiv.
 Register IZR as reals.R.IZR.
 Register Rabs as reals.R.Rabs.
-Register sqrt as reals.R.sqrt.
 Register powerRZ as reals.R.powerRZ.
+Register pow as reals.R.pow.
+Register Qreals.Q2R as reals.R.Q2R.
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 0b3656f5865d..78b26c83ea47 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -44,6 +44,7 @@ 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 pow as num.Z.pow.
 Register of_nat as num.Z.of_nat.
 
 (** When including property functors, only inline t eq zero one two *)
diff --git a/theories/micromega/DeclConstant.v b/theories/micromega/DeclConstant.v
index bd8490d79620..2e50481b13ac 100644
--- a/theories/micromega/DeclConstant.v
+++ b/theories/micromega/DeclConstant.v
@@ -35,6 +35,7 @@ Require Import List.
 (** Ground terms (see [GT] below) are built inductively from declared constants. *)
 
 Class DeclaredConstant {T : Type} (F : T).
+Register DeclaredConstant as micromega.DeclaredConstant.type.
 
 Class GT {T : Type} (F : T).
 
diff --git a/theories/micromega/EnvRing.v b/theories/micromega/EnvRing.v
index 28c7e8c55482..7bef11e89a69 100644
--- a/theories/micromega/EnvRing.v
+++ b/theories/micromega/EnvRing.v
@@ -31,6 +31,14 @@ Inductive PExpr {C} : Type :=
 | PEpow : PExpr -> N -> PExpr.
 Arguments PExpr : clear implicits.
 
+Register PEc as micromega.PExpr.PEc.
+Register PEX as micromega.PExpr.PEX.
+Register PEadd as micromega.PExpr.PEadd.
+Register PEsub as micromega.PExpr.PEsub.
+Register PEmul as micromega.PExpr.PEmul.
+Register PEopp as micromega.PExpr.PEopp.
+Register PEpow as micromega.PExpr.PEpow.
+
  (* Definition of multivariable polynomials with coefficients in C :
     Type [Pol] represents [X1 ... Xn].
     The representation is Horner's where a [n] variable polynomial
@@ -60,6 +68,10 @@ Inductive Pol {C} : Type :=
 | PX : Pol -> positive -> Pol -> Pol.
 Arguments Pol : clear implicits.
 
+Register Pc as micromega.Pol.Pc.
+Register Pinj as micromega.Pol.Pinj.
+Register PX   as micromega.Pol.PX.
+
 Section MakeRingPol.
 
  (* Ring elements *)
diff --git a/theories/micromega/Lra.v b/theories/micromega/Lra.v
index 22cef50e0d24..5c8cece845e2 100644
--- a/theories/micromega/Lra.v
+++ b/theories/micromega/Lra.v
@@ -20,6 +20,7 @@ Require Import Rdefinitions.
 Require Import RingMicromega.
 Require Import VarMap.
 Require Coq.micromega.Tauto.
+Require Import Rregisternames.
 Declare ML Module "micromega_plugin".
 
 Ltac rchange := 
diff --git a/theories/micromega/QMicromega.v b/theories/micromega/QMicromega.v
index e28de1a620aa..1fbc5a648a5a 100644
--- a/theories/micromega/QMicromega.v
+++ b/theories/micromega/QMicromega.v
@@ -154,6 +154,9 @@ Qed.
 
 Definition QWitness := Psatz Q.
 
+Register QWitness as micromega.QWitness.type.
+
+
 Definition QWeakChecker := check_normalised_formulas 0 1 Qplus Qmult Qeq_bool Qle_bool.
 
 Require Import List.
diff --git a/theories/micromega/RMicromega.v b/theories/micromega/RMicromega.v
index a67c273c7f43..fd8903eac992 100644
--- a/theories/micromega/RMicromega.v
+++ b/theories/micromega/RMicromega.v
@@ -150,7 +150,17 @@ Inductive Rcst :=
   | CInv  (r : Rcst)
   | COpp  (r : Rcst).
 
-
+Register Rcst   as micromega.Rcst.type.
+Register C0     as micromega.Rcst.C0.
+Register C1     as micromega.Rcst.C1.
+Register CQ     as micromega.Rcst.CQ.
+Register CZ     as micromega.Rcst.CZ.
+Register CPlus  as micromega.Rcst.CPlus.
+Register CMinus as micromega.Rcst.CMinus.
+Register CMult  as micromega.Rcst.CMult.
+Register CPow   as micromega.Rcst.CPow.
+Register CInv   as micromega.Rcst.CInv.
+Register COpp   as micromega.Rcst.COpp.
 
 Definition z_of_exp (z : Z + nat) :=
   match z with
diff --git a/theories/micromega/RingMicromega.v b/theories/micromega/RingMicromega.v
index 04de9509acfa..fb7fbcf80ba9 100644
--- a/theories/micromega/RingMicromega.v
+++ b/theories/micromega/RingMicromega.v
@@ -298,6 +298,15 @@ Inductive Psatz : Type :=
 | PsatzC    : C -> Psatz
 | PsatzZ    : Psatz.
 
+Register PsatzIn     as micromega.Psatz.PsatzIn.
+Register PsatzSquare as micromega.Psatz.PsatzSquare.
+Register PsatzMulC   as micromega.Psatz.PsatzMulC.
+Register PsatzMulE   as micromega.Psatz.PsatzMulE.
+Register PsatzAdd    as micromega.Psatz.PsatzAdd.
+Register PsatzC      as micromega.Psatz.PsatzC.
+Register PsatzZ      as micromega.Psatz.PsatzZ.
+
+
 (** Given a list [l] of NFormula and an extended polynomial expression
    [e], if [eval_Psatz l e] succeeds (= Some f) then [f] is a
    logic consequence of the conjunction of the formulae in l.
@@ -672,6 +681,13 @@ Inductive Op2 : Set := (* binary relations *)
 | OpLt
 | OpGt.
 
+Register OpEq  as micromega.Op2.OpEq.
+Register OpNEq as micromega.Op2.OpNEq.
+Register OpLe  as micromega.Op2.OpLe.
+Register OpGe  as micromega.Op2.OpGe.
+Register OpLt  as micromega.Op2.OpLt.
+Register OpGt  as micromega.Op2.OpGt.
+
 Definition eval_op2 (o : Op2) : R -> R -> Prop :=
 match o with
 | OpEq => req
@@ -686,12 +702,15 @@ Definition  eval_pexpr : PolEnv -> PExpr C -> R :=
  PEeval rplus rtimes rminus ropp phi pow_phi rpow.
 
 #[universes(template)]
-Record Formula (T:Type) : Type := {
+Record Formula (T:Type) : Type := Build_Formula{
   Flhs : PExpr T;
   Fop : Op2;
   Frhs : PExpr T
 }.
 
+Register Formula as micromega.Formula.type.
+Register Build_Formula as micromega.Formula.Build_Formula.
+
 Definition eval_formula (env : PolEnv) (f : Formula C) : Prop :=
   let (lhs, op, rhs) := f in
     (eval_op2 op) (eval_pexpr env lhs) (eval_pexpr env rhs).
diff --git a/theories/micromega/Tauto.v b/theories/micromega/Tauto.v
index a3e3cc3e9d11..6e8908935595 100644
--- a/theories/micromega/Tauto.v
+++ b/theories/micromega/Tauto.v
@@ -37,6 +37,16 @@ Section S.
   | N    : GFormula  -> GFormula
   | I    : GFormula  -> option AF -> GFormula  -> GFormula.
 
+  Register TT as micromega.GFormula.TT.
+  Register FF as micromega.GFormula.FF.
+  Register X  as micromega.GFormula.X.
+  Register A  as micromega.GFormula.A.
+  Register Cj as micromega.GFormula.Cj.
+  Register D  as micromega.GFormula.D.
+  Register N  as micromega.GFormula.N.
+  Register I  as micromega.GFormula.I.
+
+
   Section MAPX.
     Variable F : TX -> TX.
 
@@ -137,6 +147,8 @@ End S.
 (** Typical boolean formulae *)
 Definition BFormula (A : Type) := @GFormula A Prop unit unit.
 
+Register BFormula as micromega.BFormula.type.
+
 Section MAPATOMS.
   Context {TA TA':Type}.
   Context {TX  : Type}.
diff --git a/theories/micromega/VarMap.v b/theories/micromega/VarMap.v
index c2472f63030c..e28c27f4000d 100644
--- a/theories/micromega/VarMap.v
+++ b/theories/micromega/VarMap.v
@@ -33,6 +33,11 @@ Inductive t {A} : Type :=
 | Branch : t  -> A -> t  -> t .
 Arguments t : clear implicits.
 
+Register Branch as micromega.VarMap.Branch.
+Register Elt    as micromega.VarMap.Elt.
+Register Empty  as micromega.VarMap.Empty.
+Register t      as micromega.VarMap.type.
+
 Section MakeVarMap.
   
   Variable A : Type.
diff --git a/theories/micromega/ZMicromega.v b/theories/micromega/ZMicromega.v
index efb263faf380..bff9671feee7 100644
--- a/theories/micromega/ZMicromega.v
+++ b/theories/micromega/ZMicromega.v
@@ -564,10 +564,14 @@ Inductive ZArithProof :=
 .
 (*| SplitProof :   PolC Z -> ZArithProof -> ZArithProof -> ZArithProof.*)
 
+Register ZArithProof as micromega.ZArithProof.type.
+Register DoneProof   as micromega.ZArithProof.DoneProof.
+Register RatProof    as micromega.ZArithProof.RatProof.
+Register CutProof    as micromega.ZArithProof.CutProof.
+Register EnumProof   as micromega.ZArithProof.EnumProof.
+Register ExProof     as micromega.ZArithProof.ExProof.
 
 
-(* n/d <= x  -> d*x - n >= 0 *)
-
 
 (* In order to compute the 'cut', we need to express a polynomial P as a * Q + b.
    - b is the constant