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

2 files changed, 14 insertions, 2 deletions

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.