diff options
author | 2018-12-29 14:31:32 -0500 | |
---|---|---|
committer | 2018-12-29 14:31:32 -0500 | |
commit | 2708a015fcf65f72328be4296a00dd32b1f1c17a (patch) | |
tree | 696f9b5fb84817e1a5c8d9271976a92e25aef18a /test-suite/output/Notations.v | |
parent | d7d80c5bea564b7cb0eadc33e9ee38c9d9de1cd8 (diff) | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Updated version 8.8.2 from 'upstream/8.8.2'
with Debian dir a16bcf46abacaf1a684eda04f02555c984bf540d
Diffstat (limited to 'test-suite/output/Notations.v')
-rw-r--r-- | test-suite/output/Notations.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v index 2ccca829..fe6c05c3 100644 --- a/test-suite/output/Notations.v +++ b/test-suite/output/Notations.v @@ -1,3 +1,14 @@ +(* Bug 5568, don't warn for notations in repeated module import *) + +Module foo. +Notation compose := (fun g f => g f). +Notation "g & f" := (compose g f) (at level 10). +End foo. + +Import foo. +Import foo. +Import foo. + (**********************************************************************) (* Notations for if and let (submitted by Roland Zumkeller) *) @@ -280,3 +291,11 @@ Check fun (x:nat) (p : x=x) => match p with ONE => ONE end = p. Notation "1" := eq_refl. Check fun (x:nat) (p : x=x) => match p with 1 => 1 end = p. +(* Check bug 5693 *) + +Module M. +Definition A := 0. +Definition bar (a b : nat) := plus a b. +Notation "" := A (format "", only printing). +Check (bar A 0). +End M. |