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

1 files changed, 15 insertions, 0 deletions

diff --git a/theories/QArith/QArith_base.v b/theories/QArith/QArith_base.v
index bd5225d9ef..74cdd1797c 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.