aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/ZSyntax.out
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-01-25 19:26:59 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-01-25 19:26:59 +0000
commited37638fe1b57f1e5866b21e8a009c23802e9fec (patch)
treef0bb94a52df2467d5e34f3574ec604cf53280bb6 /test-suite/output/ZSyntax.out
parent208e7b9690337ada5598b0c9751928c1eae9bb6e (diff)
Test affichage O de nat dans une expression sur Z
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2440 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/ZSyntax.out')
-rw-r--r--test-suite/output/ZSyntax.out2
1 files changed, 2 insertions, 0 deletions
diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out
index c1a9e1161..7ef79aba4 100644
--- a/test-suite/output/ZSyntax.out
+++ b/test-suite/output/ZSyntax.out
@@ -1,2 +1,4 @@
`32`
: Z
+[f:(nat->Z)]`(f O)+0`
+ : (nat->Z)->Z