diff options
Diffstat (limited to 'test-suite/output/Notations3.v')
| -rw-r--r-- | test-suite/output/Notations3.v | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 3cf0c913f..876aaa394 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -385,3 +385,17 @@ Module LocateNotations. Locate "exists". Locate "( _ , _ , .. , _ )". End LocateNotations. + +Module Issue7731. + +Axiom (P : nat -> Prop). +Parameter (X : nat). +Notation "## @ E ^^^" := (P E) (at level 20, E at level 1, format "'[ ' ## '/' @ E '/' ^^^ ']'"). +Notation "%" := X. + +Set Printing Width 7. +Goal ## @ % ^^^. +Show. +Abort. + +End Issue7731. |