diff options
Diffstat (limited to 'test-suite/micromega/example.v')
| -rw-r--r-- | test-suite/micromega/example.v | 5 |
1 files changed, 2 insertions, 3 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. |