diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-04 15:06:00 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-12-04 15:06:00 +0000 |
| commit | 2b6ce061e6c9170bdaf74633edc8323512f1d456 (patch) | |
| tree | 82e5c8c53d21a46b17c59905dc3fd3e05ce64226 /test-suite/success/Notations.v | |
| parent | aea34fdc7caec6faf9cf54e70ae33631357ec0f1 (diff) | |
Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).
Thanks to Marc Lasson for the analysis of the problem and for the
initial patch.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13679 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/success/Notations.v')
| -rw-r--r-- | test-suite/success/Notations.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v index 661a8757a..18e2479e5 100644 --- a/test-suite/success/Notations.v +++ b/test-suite/success/Notations.v @@ -59,3 +59,10 @@ Check (fun x:nat*nat => match x with R x y => (x,y) end). Local Notation "[ a # ; .. # ; b ]" := (a + .. (b + 0) ..). Check [ 0 ]. Check [ 0 # ; 1 ]. + +(* Check well-scoping of alpha-renaming of private binders *) +(* see bug #2248 (thanks to Marc Lasson) *) + +Notation "{ q , r | P }" := (fun (p:nat*nat), let (q, r) := p in P). +Check (fun p, {q,r| q + r = p}). + |