summaryrefslogtreecommitdiff
path: root/test-suite/success/ROmega.v
diff options
context:
space:
mode:
authorGravatar Samuel Mimram <smimram@debian.org>2007-08-18 20:34:57 +0000
committerGravatar Samuel Mimram <smimram@debian.org>2007-08-18 20:34:57 +0000
commit72b9a7df489ea47b3e5470741fd39f6100d31676 (patch)
tree60108a573d2a80d2dd4e3833649890e32427ff8d /test-suite/success/ROmega.v
parent55ce117e8083477593cf1ff2e51a3641c7973830 (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.v14
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 *)