3 files changed, 28 insertions, 2 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.
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index da14358ef..c361eb4dc 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1312,8 +1312,15 @@ let make_pa_rule level (typs,symbols) ntn need_squash =
 
 let make_pp_rule level (typs,symbols) fmt =
   match fmt with
-  | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols level)]
-  | Some fmt -> hunks_of_format (level, List.split typs) (symbols, parse_format fmt)
+  | None ->
+     let hunks = make_hunks typs symbols level in
+     if List.exists (function _,(UnpCut (PpBrk _) | UnpListMetaVar _) -> true | _ -> false) hunks then
+       [UnpBox (PpHOVB 0,hunks)]
+     else
+       (* Optimization to work around what seems an ocaml Format bug (see Mantis #7804/#7807) *)
+       List.map snd hunks (* drop locations which are dummy *)
+  | Some fmt ->
+     hunks_of_format (level, List.split typs) (symbols, parse_format fmt)
 
 (* let make_syntax_rules i_typs (ntn,prec,need_squash) sy_data fmt extra onlyprint compat = *)
 let make_syntax_rules (sd : SynData.syn_data) = let open SynData in