aboutsummaryrefslogtreecommitdiff
path: root/test-suite/output/ZSyntax.out
diff options
context:
space:
mode:
authornotin2008-03-26 17:22:36 +0000
committernotin2008-03-26 17:22:36 +0000
commit57eec1e1e4efd09f5181297d87b1908c284e6951 (patch)
tree043c9810a48393013b774f7335129b83c56c6bc4 /test-suite/output/ZSyntax.out
parentc9398a44487f406e03179ecedd768698adcb1903 (diff)
Diverses petites modifs dans la test-suite:
test-suite/output/ZSyntax.out typo test-suite/bugs/closed/shouldsucceed/1776.v bug closed test-suite/success/extraction.v test-suite/success/extraction.v test-suite/bugs/closed/shouldsucceed/846.v backtrack sur le commit 10639 test-suite/bugs/closed/shouldsucceed/1322.v: petites modifications suite aux changement de setoid_replace test-suite/bugs/closed/shouldsucceed/1414.v: petites modifications suite aux changement dans Program git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10723 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 a24ad124eb..f23198b0f3 100644
--- a/test-suite/output/ZSyntax.out
+++ b/test-suite/output/ZSyntax.out
@@ -2,7 +2,7 @@
: Z
fun f : nat -> Z => (f 0%nat + 0)%Z
: (nat -> Z) -> Z
-fun x : positive => Zpos x~0)
+fun x : positive => Zpos x~0
: positive -> Z
fun x : positive => (Zpos x + 1)%Z
: positive -> Z