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.out | |
| 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.out')
| -rw-r--r-- | test-suite/output/Notations2.out | 6 |
1 files changed, 6 insertions, 0 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 |