diff options
Diffstat (limited to 'test-suite/output/Notations3.v')
| -rw-r--r-- | test-suite/output/Notations3.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 4b8bfe3124..5676fe8c7c 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -139,3 +139,9 @@ Notation "'tele' x .. z := b" := (at level 85, x binder, z binder). Check tele (t:Type) '((y,z):nat*nat) (x:t) := tt. + +(**********************************************************************) +(* Test printing of #5526 *) + +Notation "x === x" := (eq_refl x) (only printing, at level 10). +Check (fun x => eq_refl x). |