3 files changed, 27 insertions, 13 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index ffea0819a5..a9ae74fd67 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -109,3 +109,9 @@ fun x : ?A => x === x
      : forall x : ?A, x = x
 where
 ?A : [x : ?A |- Type] (x cannot be used)
+{0, 1}
+     : nat * nat
+{0, 1, 2}
+     : nat * (nat * nat)
+{0, 1, 2, 3}
+     : nat * (nat * (nat * nat))
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 250aecafd4..dee0f70f79 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -160,3 +160,11 @@ End Bug4765.
 
 Notation "x === x" := (eq_refl x) (only printing, at level 10).
 Check (fun x => eq_refl x).
+
+(**********************************************************************)
+(* Test recursive notations with the recursive pattern repeated on the right *)
+
+Notation "{ x , .. , y , z }" := (pair x .. (pair y z) ..).
+Check {0,1}.
+Check {0,1,2}.
+Check {0,1,2,3}.
diff --git a/test-suite/output/TypeclassDebug.out b/test-suite/output/TypeclassDebug.out
index 73369ab713..8b38fe0ff4 100644
--- a/test-suite/output/TypeclassDebug.out
+++ b/test-suite/output/TypeclassDebug.out
@@ -1,18 +1,18 @@
 Debug: 1: looking for foo without backtracking
 Debug: 1.1: simple apply H on foo, 1 subgoal(s)
-Debug: 1.1-2 : foo
-Debug: 1.1-2: looking for foo without backtracking
-Debug: 1.1-2.1: simple apply H on foo, 1 subgoal(s)
-Debug: 1.1-2.1-2 : foo
-Debug: 1.1-2.1-2: looking for foo without backtracking
-Debug: 1.1-2.1-2.1: simple apply H on foo, 1 subgoal(s)
-Debug: 1.1-2.1-2.1-2 : foo
-Debug: 1.1-2.1-2.1-2: looking for foo without backtracking
-Debug: 1.1-2.1-2.1-2.1: simple apply H on foo, 1 subgoal(s)
-Debug: 1.1-2.1-2.1-2.1-2 : foo
-Debug: 1.1-2.1-2.1-2.1-2: looking for foo without backtracking
-Debug: 1.1-2.1-2.1-2.1-2.1: simple apply H on foo, 1 subgoal(s)
-Debug: 1.1-2.1-2.1-2.1-2.1-2 : foo
+Debug: 1.1-1 : foo
+Debug: 1.1-1: looking for foo without backtracking
+Debug: 1.1-1.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-1.1-1 : foo
+Debug: 1.1-1.1-1: looking for foo without backtracking
+Debug: 1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-1.1-1.1-1 : foo
+Debug: 1.1-1.1-1.1-1: looking for foo without backtracking
+Debug: 1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-1.1-1.1-1.1-1 : foo
+Debug: 1.1-1.1-1.1-1.1-1: looking for foo without backtracking
+Debug: 1.1-1.1-1.1-1.1-1.1: simple apply H on foo, 1 subgoal(s)
+Debug: 1.1-1.1-1.1-1.1-1.1-1 : foo
 The command has indeed failed with message:
 Ltac call to "typeclasses eauto (int_or_var_opt) with (ne_preident_list)" failed.
 Tactic failure: Proof search reached its limit.