aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/ZSyntax.out
diff options
context:
space:
mode:
authorGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-10-16 15:59:10 +0000
committerGravatar herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>2002-10-16 15:59:10 +0000
commiteb91c10a612da48654127c6aba3838caee0a9ce0 (patch)
tree951f9f931af561b84f216f5ce56e96898f31accb /test-suite/output/ZSyntax.out
parent246d622a0e6ca08bd659e46ecaa01a2345e03a03 (diff)
Parseur pour n>20 dans nat plus disponible
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3152 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/ZSyntax.out')
-rw-r--r--test-suite/output/ZSyntax.out2
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out
index 9774f20cf..0fdc5b7e3 100644
--- a/test-suite/output/ZSyntax.out
+++ b/test-suite/output/ZSyntax.out
@@ -22,5 +22,5 @@
: Z
`(inject_nat (0)) = 0`
: Prop
-`0+(inject_nat (789))`
+`0+(inject_nat (11))`
: Z