Micromega: doc + test-suite update

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

3 files changed, 3 insertions, 3 deletions

diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v
index 905b9a938..751fe91ed 100644
--- a/test-suite/micromega/example.v
+++ b/test-suite/micromega/example.v
@@ -333,7 +333,7 @@ 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 ; sos Z.
+  intros ; psatz Z.
 Qed.
 
 
diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v
index 8a349a1d9..1fa250e09 100644
--- a/test-suite/micromega/qexample.v
+++ b/test-suite/micromega/qexample.v
@@ -72,7 +72,7 @@ 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 ; sos Q.
+  intros ; psatz Q.
 Qed.
 
 
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v
index 1de1955db..d7386a4ec 100644
--- a/test-suite/micromega/rexample.v
+++ b/test-suite/micromega/rexample.v
@@ -69,7 +69,7 @@ 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 ; sos R.
+  intros ; psatz R.
 Qed.
 
 Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z).