Ajout d'une version nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6451 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 17 insertions, 0 deletions

diff --git a/test-suite/output/ZSyntax.v8 b/test-suite/output/ZSyntax.v8
new file mode 100644
index 0000000000..0412f6d68e
--- /dev/null
+++ b/test-suite/output/ZSyntax.v8
@@ -0,0 +1,17 @@
+Require Import ZArith.
+Check 32%Z.
+Check (fun f : nat -> Z => (f 0%nat + 0)%Z).
+Check (fun x : positive => Zpos (xO x)).
+Check (fun x : positive => (Zpos x + 1)%Z).
+Check (fun x : positive => Zpos x).
+Check (fun x : positive => Zneg (xO x)).
+Check (fun x : positive => (Zpos (xO x) + 0)%Z).
+Check (fun x : positive => (- Zpos (xO x))%Z).
+Check (fun x : positive => (- Zpos (xO x) + 0)%Z).
+Check (Z_of_nat 0 + 1)%Z.
+Check (0 + Z_of_nat (0 + 0))%Z.
+Check (Z_of_nat 0 = 0%Z).
+
+(* Submitted by Pierre Casteran *)
+Require Import Arith.
+Check (0 + Z_of_nat 11)%Z.
\ No newline at end of file