From ca1305a0187653edcf63e46b84c65130ac78d117 Mon Sep 17 00:00:00 2001
From: Frédéric Besson
Date: Fri, 20 Dec 2013 01:22:45 +0100
Subject: micromega: removal of spurious Export; addition of Lia.v
 encapsulating lia and nia.

---
 test-suite/micromega/heap3_vcgen_25.v | 2 +-
 test-suite/micromega/zomicron.v       | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/micromega/heap3_vcgen_25.v b/test-suite/micromega/heap3_vcgen_25.v
index efb5c7fd5c..00522f50aa 100644
--- a/test-suite/micromega/heap3_vcgen_25.v
+++ b/test-suite/micromega/heap3_vcgen_25.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 Require Import ZArith.
-Require Import Psatz.
+Require Import Lia.
 
 Open Scope Z_scope.
 
diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v
index 3b24602336..0ec1dbfbcd 100644
--- a/test-suite/micromega/zomicron.v
+++ b/test-suite/micromega/zomicron.v
@@ -1,5 +1,5 @@
 Require Import ZArith.
-Require Import Psatz.
+Require Import Lia.
 Open Scope Z_scope.
 
 Lemma two_x_eq_1 : forall x, 2 * x = 1 -> False.
-- 
cgit v1.2.3