diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-10 10:53:32 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-06-29 19:14:07 +0200 |
| commit | e3a7caa0fb44f7a12248a140528462853810a614 (patch) | |
| tree | 6b8efab5834d07308ecd5b2cc19a810d13c376a1 /test-suite/output | |
| parent | d46dd57462650d1e956d8e80d5aa4e537205de4d (diff) | |
Workaround to fix #7731 (printing not splitting line at break hint).
In some cases, Format's inner boxes inside an outer box act as break
hints, even though there are already "better" break hints in the outer
box.
We work around this "feature" by not inserting a box around the
default printing rule for a notation if there is no effective break
points in the box.
See https://caml.inria.fr/mantis/view.php?id=7804 for the related
OCaml discussion.
Diffstat (limited to 'test-suite/output')
| -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. |