summaryrefslogtreecommitdiff
path: root/test-suite/success/ROmega.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
committerGravatar Samuel Mimram <smimram@debian.org>2008-07-25 15:12:53 +0200
commita0cfa4f118023d35b767a999d5a2ac4b082857b4 (patch)
treedabcac548e299fee1da464c93b3dba98484f45b1 /test-suite/success/ROmega.v
parent2281410e38ef99d025ea77194585a9bc019fdaa9 (diff)
Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg
Diffstat (limited to 'test-suite/success/ROmega.v')
-rw-r--r--test-suite/success/ROmega.v20
1 files changed, 9 insertions, 11 deletions
diff --git a/test-suite/success/ROmega.v b/test-suite/success/ROmega.v
index ff1f57df..0c37c59a 100644
--- a/test-suite/success/ROmega.v
+++ b/test-suite/success/ROmega.v
@@ -68,31 +68,29 @@ Variable n : nat.
Variable ap_n : n <> 0.
Let delta := f n ap_n.
Lemma lem7 : n = n.
- (*romega. ---> ROMEGA CANT DEAL WITH NAT*)
-Admitted.
+ romega with nat.
+Qed.
End C.
(* Problem of dependencies *)
Require Import Omega.
Lemma lem8 : forall H : 0 = 0 -> 0 = 0, H = H -> 0 = 0.
intros.
-(* romega. ---> ROMEGA CANT DEAL WITH NAT*)
-Admitted.
+romega with nat.
+Qed.
(* Bug that what caused by the use of intro_using in Omega *)
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*)
-Admitted.
+romega with nat.
+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; romega with nat.
Qed.
-*)