diff options
| author |  fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-02 13:24:47 +0000 |
|---|---|---|
| committer | fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-07-02 13:24:47 +0000 |
| commit | 3bf96f48739699da368bb872663945ebdb2d78a4 (patch) | |
| tree | 7d29f2a7a70a3b345bdc3587fe2563d6a586576d /test-suite/micromega/rexample.v | |
| parent | 7f110df7d7ff6a4d43f3c8d19305b20e24f4800e (diff) | |
Improved robustness of micromega parser. Proof search of Micromega test-suites is now bounded -- ensure termination
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11200 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/micromega/rexample.v')
| -rw-r--r-- | test-suite/micromega/rexample.v | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v index 5738ebbff..1de1955db 100644 --- a/test-suite/micromega/rexample.v +++ b/test-suite/micromega/rexample.v @@ -12,7 +12,7 @@ Require Import Ring_normalize. Open Scope R_scope. -Lemma plus_minus : forall x y, +Lemma yplus_minus : forall x y, 0 = x + y -> 0 = x -y -> 0 = x /\ 0 = y. Proof. intros. @@ -74,10 +74,4 @@ Qed. Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z). intros; split_Rabs; psatzl R. -Qed. - -Lemma l2 : - forall x y : R, x < Rabs y -> y < 1 -> x >= 0 -> - y <= 1 -> Rabs x <= 1. -intros. -split_Rabs; psatzl R. -Qed. +Qed.
\ No newline at end of file |