Micromega: qualify Coq.micromega.Tauto (avoid coqdep warnings about new Init/Tauto.v)

6 files changed, 6 insertions, 6 deletions

diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v
index 3e58e81ac..52bf5ed3d 100644
--- a/plugins/micromega/Lia.v
+++ b/plugins/micromega/Lia.v
@@ -16,7 +16,7 @@ Require Import ZMicromega.
 Require Import ZArith.
 Require Import RingMicromega.
 Require Import VarMap.
-Require Tauto.
+Require Coq.micromega.Tauto.
 Declare ML Module "micromega_plugin".
 
 Ltac preprocess :=
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index ba1f8956e..fafd8a5f2 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -20,7 +20,7 @@ Require Import ZArith.
 Require Import Rdefinitions.
 Require Import RingMicromega.
 Require Import VarMap.
-Require Tauto.
+Require Coq.micromega.Tauto.
 Declare ML Module "micromega_plugin".
 
 Ltac preprocess := 
diff --git a/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v
index 432683635..b13285f53 100644
--- a/plugins/micromega/QMicromega.v
+++ b/plugins/micromega/QMicromega.v
@@ -168,7 +168,7 @@ Proof.
   exact H.
 Qed.
 
-Require Import Tauto.
+Require Import Coq.micromega.Tauto.
 
 Definition Qnormalise := @cnf_normalise Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool.
 Definition Qnegate := @cnf_negate Q 0 1 Qplus Qmult Qminus Qopp Qeq_bool.
diff --git a/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v
index 72353a99e..2352d78d6 100644
--- a/plugins/micromega/RMicromega.v
+++ b/plugins/micromega/RMicromega.v
@@ -533,7 +533,7 @@ Proof.
   exact H.
 Qed.
 
-Require Import Tauto.
+Require Import Coq.micromega.Tauto.
 
 Definition Rnormalise := @cnf_normalise Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq_bool.
 Definition Rnegate := @cnf_negate Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq_bool.
diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 751a81df1..ed49c3df4 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -794,7 +794,7 @@ Definition xnormalise (t:Formula C) : list (NFormula)  :=
       | OpLe => (psub lhs rhs ,Strict) :: nil
     end.
 
-Require Import Tauto.
+Require Import Coq.micromega.Tauto.
 
 Definition cnf_normalise (t:Formula C) : cnf (NFormula) :=
   List.map  (fun x => x::nil) (xnormalise t).
diff --git a/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index d7ddef2be..5aa8d03f9 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -198,7 +198,7 @@ Definition xnormalise (t:Formula Z) : list (NFormula Z)  :=
       | OpLe => (psub lhs (padd rhs (Pc 1)),NonStrict) :: nil
     end.
 
-Require Import Tauto BinNums.
+Require Import Coq.micromega.Tauto BinNums.
 
 Definition normalise (t:Formula Z) : cnf (NFormula Z) :=
   List.map  (fun x => x::nil) (xnormalise t).