From 8f4b002c44c4820131acd929d31502ab7cf952c4 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 14 Jun 2010 09:29:47 +0000 Subject: 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 --- test-suite/output/Notations2.out | 6 ++++++ test-suite/output/Notations2.v | 10 ++++++++-- 2 files changed, 14 insertions(+), 2 deletions(-) (limited to 'test-suite') diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out index c1a7e961a..20d20d826 100644 --- a/test-suite/output/Notations2.out +++ b/test-suite/output/Notations2.out @@ -4,3 +4,9 @@ : nat forall (A : Set) (le : A -> A -> Prop) (x y : A), le x y \/ le y x : Prop +match (0, 0, 0) with +| (x, y, z) => x + y + z +end + : nat +let '(a, _, _) := (2, 3, 4) in a + : nat 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. -- cgit v1.2.3