2 files changed, 34 insertions, 0 deletions
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index 799d310fa7..43f88f42a5 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -63,3 +63,11 @@ fun '{| |} => true
      : R -> bool
 b = a
      : Prop
+The command has indeed failed with message:
+The format is not the same on the right- and left-hand sides of the special token "..".
+The command has indeed failed with message:
+The format is not the same on the right- and left-hand sides of the special token "..".
+The command has indeed failed with message:
+The format is not the same on the right- and left-hand sides of the special token "..".
+The command has indeed failed with message:
+The format is not the same on the right- and left-hand sides of the special token "..".
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 26c7840a16..4de6ce19b4 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -158,3 +158,29 @@ Check b = a.
 End Test.
 
 End L.
+
+Module M.
+
+(* Accept boxes around the end variables of a recursive notation (if equal boxes) *)
+
+Notation " {@ T1 ; T2 ; .. ; Tn } " :=
+  (and T1 (and T2 .. (and Tn True)..))
+  (format "'[v' {@  '[' T1 ']'  ;  '//' '['  T2  ']'  ;  '//' ..  ;   '//' '['  Tn  ']'  } ']'").
+
+Fail Notation " {@ T1 ; T2 ; .. ; Tn } " :=
+  (and T1 (and T2 .. (and Tn True)..))
+  (format "'[v' {@  '[' T1 ']'  ;  '//' '['  T2  ']'  ;  '//' ..  ;   '//' '['  Tn   ']'  } ']'").
+
+Fail Notation " {@ T1 ; T2 ; .. ; Tn } " :=
+  (and T1 (and T2 .. (and Tn True)..))
+  (format "'[v' {@  '[' T1 ']'  ;  '//' '['  T2  ']'  ;  '//' ..  ;   '//' '[v'  Tn  ']'  } ']'").
+
+Fail Notation " {@ T1 ; T2 ; .. ; Tn } " :=
+  (and T1 (and T2 .. (and Tn True)..))
+  (format "'[v' {@  '[' T1 ']'  ;  '//' '['  T2  ']'  ;  '//' ..  ;   '//' '['   Tn  ']'  } ']'").
+
+Fail Notation " {@ T1 ; T2 ; .. ; Tn } " :=
+  (and T1 (and T2 .. (and Tn True)..))
+  (format "'[v' {@  '[' T1 ']'  ;  '//' '['  T2  ']'   ;  '//' ..  ;   '//' '['  Tn  ']'  } ']'").
+
+End M.