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/bertot.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/bertot.v')
| -rw-r--r-- | test-suite/micromega/bertot.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/micromega/bertot.v b/test-suite/micromega/bertot.v index 8e9c0c6de..bcf222f92 100644 --- a/test-suite/micromega/bertot.v +++ b/test-suite/micromega/bertot.v @@ -17,6 +17,6 @@ Goal (forall x y n, (x < n /\ x <= n /\ 2 * y = x * (x+1) -> x + 1 <= n /\ 2 *(x+1+y) = (x+1)*(x+2))). Proof. intros. - psatz Z. + psatz Z 3. Qed. |