diff options
Diffstat (limited to 'test-suite/micromega')
-rw-r--r-- | test-suite/micromega/example.v | 5 | ||||
-rw-r--r-- | test-suite/micromega/heap3_vcgen_25.v | 2 | ||||
-rw-r--r-- | test-suite/micromega/qexample.v | 1 | ||||
-rw-r--r-- | test-suite/micromega/rexample.v | 1 | ||||
-rw-r--r-- | test-suite/micromega/zomicron.v | 2 |
5 files changed, 4 insertions, 7 deletions
diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v index d648c2e4..25e4a09f 100644 --- a/test-suite/micromega/example.v +++ b/test-suite/micromega/example.v @@ -2,13 +2,12 @@ (* *) (* Micromega: A reflexive tactic using the Positivstellensatz *) (* *) -(* Frédéric Besson (Irisa/Inria) 2006-2008 *) +(* Frédéric Besson (Irisa/Inria) 2006-2008 *) (* *) (************************************************************************) Require Import ZArith. Require Import Psatz. -Require Import Ring_normalize. Open Scope Z_scope. Require Import ZMicromega. Require Import VarMap. @@ -23,7 +22,7 @@ Proof. Qed. -(* From Laurent Théry *) +(* From Laurent Théry *) Lemma some_pol : forall x, 4 * x ^ 2 + 3 * x + 2 >= 0. Proof. diff --git a/test-suite/micromega/heap3_vcgen_25.v b/test-suite/micromega/heap3_vcgen_25.v index efb5c7fd..00522f50 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/qexample.v b/test-suite/micromega/qexample.v index 76dc52e6..47e6005b 100644 --- a/test-suite/micromega/qexample.v +++ b/test-suite/micromega/qexample.v @@ -8,7 +8,6 @@ Require Import Psatz. Require Import QArith. -Require Import Ring_normalize. Lemma plus_minus : forall x y, 0 == x + y -> 0 == x -y -> 0 == x /\ 0 == y. diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v index 9bb9dacc..2eed7e95 100644 --- a/test-suite/micromega/rexample.v +++ b/test-suite/micromega/rexample.v @@ -8,7 +8,6 @@ Require Import Psatz. Require Import Reals. -Require Import Ring_normalize. Open Scope R_scope. diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v index 3b246023..0ec1dbfb 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. |