diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-01-25 14:42:51 +0100 |
| commit | 7cfc4e5146be5666419451bdd516f1f3f264d24a (patch) | |
| tree | e4197645da03dc3c7cc84e434cc31d0a0cca7056 /test-suite/micromega/example.v | |
| parent | 420f78b2caeaaddc6fe484565b2d0e49c66888e5 (diff) | |
Imported Upstream version 8.5~beta1+dfsg
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. |