diff options
| author |  Samuel Mimram <smimram@debian.org> | 2007-08-18 20:34:57 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2007-08-18 20:34:57 +0000 |
| commit | 72b9a7df489ea47b3e5470741fd39f6100d31676 (patch) | |
| tree | 60108a573d2a80d2dd4e3833649890e32427ff8d /test-suite/success/ROmega.v | |
| parent | 55ce117e8083477593cf1ff2e51a3641c7973830 (diff) | |
Imported Upstream version 8.1.pl1+dfsgupstream/8.1.pl1+dfsg
Diffstat (limited to 'test-suite/success/ROmega.v')
| -rw-r--r-- | test-suite/success/ROmega.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/test-suite/success/ROmega.v b/test-suite/success/ROmega.v index 04b666ed..ff1f57df 100644 --- a/test-suite/success/ROmega.v +++ b/test-suite/success/ROmega.v @@ -7,8 +7,8 @@ Lemma lem1 : forall x y : Z, (-5 < x < 5)%Z -> (-5 < y)%Z -> (-5 < x + y + 5)%Z. Proof. intros x y. - (*romega.*) -Admitted. +romega. +Qed. (* Proposed by Pierre Crégut *) @@ -22,8 +22,8 @@ Qed. Lemma lem3 : forall x y : Z, x = y -> (x + x)%Z = (y + y)%Z. Proof. intros. - (*romega.*) -Admitted. +romega. +Qed. (* Proposed by Jean-Christophe Filliâtre: confusion between an Omega *) (* internal variable and a section variable (June 2001) *) @@ -68,7 +68,7 @@ Variable n : nat. Variable ap_n : n <> 0. Let delta := f n ap_n. Lemma lem7 : n = n. - (*romega.*) (*ROMEGA CANT DEAL WITH NAT*) + (*romega. ---> ROMEGA CANT DEAL WITH NAT*) Admitted. End C. @@ -76,7 +76,7 @@ End C. Require Import Omega. Lemma lem8 : forall H : 0 = 0 -> 0 = 0, H = H -> 0 = 0. intros. -(* romega.*) (*ROMEGA CANT DEAL WITH NAT*) +(* romega. ---> ROMEGA CANT DEAL WITH NAT*) Admitted. (* Bug that what caused by the use of intro_using in Omega *) @@ -84,7 +84,7 @@ Require Import Omega. Lemma lem9 : forall p q : nat, ~ (p <= q /\ p < q \/ q <= p /\ p < q) -> p < p \/ p <= p. intros. -(* romega.*)(*ROMEGA CANT DEAL WITH NAT*) +(* romega. ---> ROMEGA CANT DEAL WITH NAT*) Admitted. (* Check that the interpretation of mult on nat enforces its positivity *) |