diff options
| author |  fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-30 20:31:06 +0000 |
|---|---|---|
| committer | fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-07-30 20:31:06 +0000 |
| commit | a7c0fe84f441c4b624828a2d34459ddf78e216cf (patch) | |
| tree | 28a7842f70c2018502babf394e178d78688f8123 /test-suite/micromega | |
| parent | 92a65c4943ba13df93db2661117d1ce23e0c02ba (diff) | |
psatz Z -> psatz Z 1
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12253 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/micromega')
| -rw-r--r-- | test-suite/micromega/example.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v index 751fe91ed..5cb103953 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. |