micromega: better handling of exponentiation + correction of test-suite termination bug

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12346 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 4 insertions, 4 deletions

diff --git a/test-suite/micromega/csdp.cache b/test-suite/micromega/csdp.cache
index 961d159bf..114f714f3 100644
--- a/test-suite/micromega/csdp.cache
+++ b/test-suite/micromega/csdp.cache
diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v
index c9c779f90..76dc52e6c 100644
--- a/test-suite/micromega/qexample.v
+++ b/test-suite/micromega/qexample.v
@@ -67,12 +67,12 @@ Qed.
 Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
 Proof.
   intros.
-  psatz Q 2.
+  psatz Q 3.
 Qed.
 
 Lemma motzkin' : forall x y, (x^2+y^2+1)*(x^2*y^4 + x^4*y^2 + 1 - (3 # 1) *x^2*y^2) >= 0.
 Proof.
-  intros ; psatz Q.
+  intros ; psatz Q 3.
 Qed.
 
 
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v
index c957add69..9bb9daccb 100644
--- a/test-suite/micromega/rexample.v
+++ b/test-suite/micromega/rexample.v
@@ -64,12 +64,12 @@ Qed.
 Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
 Proof.
   intros.
-  psatz R 2.
+  psatz R 3.
 Qed.
 
 Lemma motzkin' : forall x y, (x^2+y^2+1)*(x^2*y^4 + x^4*y^2 + 1 - (3 ) *x^2*y^2) >= 0.
 Proof.
-  intros ; psatz R.
+  intros ; psatz R 2.
 Qed.
 
 Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z).