[micromega] use Coqlib.lib_ref to get Coq constants.

9 files changed, 71 insertions, 4 deletions

diff --git a/theories/micromega/DeclConstant.v b/theories/micromega/DeclConstant.v
index bd8490d796..2e50481b13 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 28c7e8c554..7bef11e89a 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 3ac4772ba4..6817f9c5c7 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 e28de1a620..1fbc5a648a 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 a67c273c7f..fd8903eac9 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 04de9509ac..fb7fbcf80b 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 a3e3cc3e9d..6e89089355 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 c2472f6303..e28c27f400 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 efb263faf3..bff9671fee 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