diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-14 09:29:47 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-14 09:29:47 +0000 |
commit | 8f4b002c44c4820131acd929d31502ab7cf952c4 (patch) | |
tree | 652c63b712b5d2784adde12d9849527673f98de8 /test-suite/output/Notations2.v | |
parent | 2c9c92aac97160a40ff240dec41464ae78a6c88c (diff) |
Added printing of recursive notations in cases pattern (supported by wish 2248).
Note that the code is no longer in constrextern.ml but in topconstr.ml where
the code for reversing notations of term already was.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13132 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/Notations2.v')
-rw-r--r-- | test-suite/output/Notations2.v | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v index 3eeff401c..2e136edf1 100644 --- a/test-suite/output/Notations2.v +++ b/test-suite/output/Notations2.v @@ -10,11 +10,17 @@ Check (2 3). (* (were not working from revision 11886 to 12951) *) Record Binop := { binop :> nat -> nat -> nat }. -Class Plusop := { plusop : Binop; z : nat }. +Class Plusop := { plusop : Binop; zero : nat }. Infix "[+]" := plusop (at level 40). -Instance Plus : Plusop := {| plusop := {| binop := plus |} ; z := 0 |}. +Instance Plus : Plusop := {| plusop := {| binop := plus |} ; zero := 0 |}. Check 2[+]3. (* Test bug #2091 (variable le was printed using <= !) *) Check forall (A: Set) (le: A -> A -> Prop) (x y: A), le x y \/ le y x. + +(* Test recursive notations in cases pattern *) + +Remove Printing Let prod. +Check match (0,0,0) with (x,y,z) => x+y+z end. +Check let '(a,b,c) := ((2,3),4) in a. |