summaryrefslogtreecommitdiff
path: root/test-suite/success/ROmegaPre.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2013-05-08 18:03:54 +0200
commitdb38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch)
tree09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /test-suite/success/ROmegaPre.v
parent6e34b272d789455a9be589e27ad3a998cf25496b (diff)
parent499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff)
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'test-suite/success/ROmegaPre.v')
-rw-r--r--test-suite/success/ROmegaPre.v16
1 files changed, 8 insertions, 8 deletions
diff --git a/test-suite/success/ROmegaPre.v b/test-suite/success/ROmegaPre.v
index bd473fa6..fa659273 100644
--- a/test-suite/success/ROmegaPre.v
+++ b/test-suite/success/ROmegaPre.v
@@ -14,38 +14,38 @@ Open Scope Z_scope.
(* zify_op *)
-Goal forall a:Z, Zmax a a = a.
+Goal forall a:Z, Z.max a a = a.
intros.
romega with *.
Qed.
-Goal forall a b:Z, Zmax a b = Zmax b a.
+Goal forall a b:Z, Z.max a b = Z.max b a.
intros.
romega with *.
Qed.
-Goal forall a b c:Z, Zmax a (Zmax b c) = Zmax (Zmax a b) c.
+Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c.
intros.
romega with *.
Qed.
-Goal forall a b:Z, Zmax a b + Zmin a b = a + b.
+Goal forall a b:Z, Z.max a b + Z.min a b = a + b.
intros.
romega with *.
Qed.
-Goal forall a:Z, (Zabs a)*(Zsgn a) = a.
+Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a.
intros.
zify.
intuition; subst; romega. (* pure multiplication: omega alone can't do it *)
Qed.
-Goal forall a:Z, Zabs a = a -> a >= 0.
+Goal forall a:Z, Z.abs a = a -> a >= 0.
intros.
romega with *.
Qed.
-Goal forall a:Z, Zsgn a = a -> a = 1 \/ a = 0 \/ a = -1.
+Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1.
intros.
romega with *.
Qed.
@@ -119,7 +119,7 @@ Qed.
(* mix of datatypes *)
-Goal forall p, Z_of_N (N_of_nat (nat_of_N (Npos p))) = Zpos p.
+Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p.
intros.
romega with *.
Qed.