3 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/7712.v b/test-suite/bugs/closed/7712.v
new file mode 100644
index 0000000000..a4e9697fad
--- /dev/null
+++ b/test-suite/bugs/closed/7712.v
@@ -0,0 +1,4 @@
+(* This used to raise an anomaly *)
+
+Fail Reserved Notation "'[tele_arg' x ';' .. ';' z ]"
+       (format "[tele_arg '[hv'  x .. z ']' ]").
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 996af59270..5ab616160a 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 3cf0c913f7..876aaa3944 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.