From a7c0fe84f441c4b624828a2d34459ddf78e216cf Mon Sep 17 00:00:00 2001
From: fbesson
Date: Thu, 30 Jul 2009 20:31:06 +0000
Subject: psatz Z -> psatz Z 1

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12253 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/micromega/example.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v
index 751fe91eda..5cb1039533 100644
--- a/test-suite/micromega/example.v
+++ b/test-suite/micromega/example.v
@@ -28,7 +28,7 @@ Qed.
 Lemma some_pol : forall x, 4 * x ^ 2 + 3 * x + 2 >= 0.
 Proof.
   intros. 
-  psatz Z 2. 
+  psatz Z 2.
 Qed.
 
 
@@ -333,7 +333,8 @@ 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 Z.
+  intros.
+  psatz Z 1.
 Qed.
 
 
-- 
cgit v1.2.3