From c14e6eebc6c3696623a440cd7eaa4a8d8fe4f492 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Thu, 19 May 2016 13:10:19 +0200
Subject: Micromega: qualify Coq.micromega.Tauto (avoid coqdep warnings about
 new Init/Tauto.v)

---
 plugins/micromega/ZMicromega.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/micromega/ZMicromega.v')

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).
-- 
cgit v1.2.3