diff options
Diffstat (limited to 'test-suite')
-rw-r--r-- | test-suite/output/Notations3.out | 5 | ||||
-rw-r--r-- | test-suite/output/Notations3.v | 14 |
2 files changed, 19 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 996af5927..5ab616160 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -241,3 +241,8 @@ Notation Notation "( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope (default interpretation) +1 subgoal + + ============================ + ##@% + ^^^ 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. |