diff options
Diffstat (limited to 'test-suite/success/Omega.v')
| -rw-r--r-- | test-suite/success/Omega.v | 14 |
1 files changed, 6 insertions, 8 deletions
diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v index 2d29a835..ecbf04e4 100644 --- a/test-suite/success/Omega.v +++ b/test-suite/success/Omega.v @@ -10,14 +10,14 @@ intros x y. omega. Qed. -(* Proposed by Pierre Crégut *) +(* Proposed by Pierre Crégut *) Lemma lem2 : forall x : Z, (x < 4)%Z -> (x > 2)%Z -> x = 3%Z. intro. omega. Qed. -(* Proposed by Jean-Christophe Filliâtre *) +(* Proposed by Jean-Christophe Filliâtre *) Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z. Proof. @@ -25,7 +25,7 @@ intros. omega. Qed. -(* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *) +(* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *) (* internal variable and a section variable (June 2001) *) Section A. @@ -87,10 +87,8 @@ Qed. (* Check that the interpretation of mult on nat enforces its positivity *) (* Submitted by Hubert Thierry (bug #743) *) -(* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" -Require Omega. -Lemma lem10 : (n, m : nat) (le n (plus n (mult n m))). +(* Postponed... problem with goals of the form "(n*m=0)%nat -> (n*m=0)%Z" *) +Lemma lem10 : forall n m:nat, le n (plus n (mult n m)). Proof. -Intros; Omega. +intros; omega with *. Qed. -*) |