From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 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 d7ddef2b..5aa8d03f 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