aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite/output/ZSyntax.out
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-08 14:52:02 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2008-03-08 14:52:02 +0000
commit6164aabc75035ca21474b51ceab4e25d47395ff7 (patch)
treeebbd1dacc3ee8feb9c86a1e8edf6518ae8cf5e86 /test-suite/output/ZSyntax.out
parent16ae29315ae0f88c4926b97f8fe22bffe65aa3e1 (diff)
Fix bugs that were reopened due to the change of setoid
implementation. Mostly syntax changes when declaring parametric relations, but also some declarations were relying on "default" relations on some carrier. Added a new DefaultRelation type class that allows to do that, falling back to the last declared Equivalence relation by default. This will be bound to Add Relation in the next commit. Also, move the "left" and "right" notations in Program.Utils to "in_left" and "in_right" to avoid clashes with existing scripts. Minor change to record to allow choosing the name of the argument for the record in projections to avoid possible incompatibilities. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10639 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/ZSyntax.out')
-rw-r--r--test-suite/output/ZSyntax.out10
1 files changed, 5 insertions, 5 deletions
diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out
index cbfb9f207..a24ad124e 100644
--- a/test-suite/output/ZSyntax.out
+++ b/test-suite/output/ZSyntax.out
@@ -2,19 +2,19 @@
: Z
fun f : nat -> Z => (f 0%nat + 0)%Z
: (nat -> Z) -> Z
-fun x : positive => Zpos (xO x)
+fun x : positive => Zpos x~0)
: positive -> Z
fun x : positive => (Zpos x + 1)%Z
: positive -> Z
fun x : positive => Zpos x
: positive -> Z
-fun x : positive => Zneg (xO x)
+fun x : positive => Zneg x~0
: positive -> Z
-fun x : positive => (Zpos (xO x) + 0)%Z
+fun x : positive => (Zpos x~0 + 0)%Z
: positive -> Z
-fun x : positive => (- Zpos (xO x))%Z
+fun x : positive => (- Zpos x~0)%Z
: positive -> Z
-fun x : positive => (- Zpos (xO x) + 0)%Z
+fun x : positive => (- Zpos x~0 + 0)%Z
: positive -> Z
(Z_of_nat 0 + 1)%Z
: Z