diff options
| author | fbesson | 2008-07-07 15:36:09 +0000 |
|---|---|---|
| committer | fbesson | 2008-07-07 15:36:09 +0000 |
| commit | d8d585d692880cfb1a9af7245346dc43d515319d (patch) | |
| tree | 897531d87362d68f417772ad868676199fa22686 /test-suite/micromega/example.v | |
| parent | cf69befd5678b6827126ef0a2b89218ea7b02c89 (diff) | |
Micromega: doc + test-suite update
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11211 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/micromega/example.v')
| -rw-r--r-- | test-suite/micromega/example.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v index 905b9a9381..751fe91eda 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. |