diff options
Diffstat (limited to 'test-suite/output/Notations3.v')
| -rw-r--r-- | test-suite/output/Notations3.v | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 4b8bfe312..96d831944 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -139,3 +139,8 @@ Notation "'tele' x .. z := b" := (at level 85, x binder, z binder). Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt. + +(* Cyprien's part of bug #4765 *) + +Notation foo5 x T y := (fun x : T => y). +Check foo5 x nat x. |