4 files changed, 22 insertions, 1 deletions
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index c012a86b01..95be04c32c 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -37,3 +37,5 @@ fun '(x, y) '(z, t) => swap (x, y) = (z, t)
      : A * B -> B * A -> Prop
 forall '(x, y) '(z, t), swap (x, y) = (z, t)
      : Prop
+fun (pat : nat) '(x, y) => x + y = pat
+     : nat -> nat * nat -> Prop
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
index 6fa357a90c..0bad472f41 100644
--- a/test-suite/output/PatternsInBinders.v
+++ b/test-suite/output/PatternsInBinders.v
@@ -64,3 +64,6 @@ Check fun '((x,y) : A*B) '(z,t) => swap (x,y) = (z,t).
 Check forall '(x,y) '((z,t) : B*A), swap (x,y) = (z,t).
 
 End Suboptimal.
+
+(** Test risk of collision for internal name *)
+Check fun pat => fun '(x,y) => x+y = pat.
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 81fda176ec..7446c17d98 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -98,6 +98,14 @@ h: n <> newdef n
 h': newdef n <> n
 h: n <> newdef n
 h: n <> newdef n
+h: n <> newdef n
+h': newdef n <> n
+The command has indeed failed with message:
+No such goal.
+The command has indeed failed with message:
+Query commands only support the single numbered goal selector.
+The command has indeed failed with message:
+Query commands only support the single numbered goal selector.
 h: P n
 h': ~ P n
 h: P n
diff --git a/test-suite/output/Search.v b/test-suite/output/Search.v
index 2a0f0b407c..82096f29bf 100644
--- a/test-suite/output/Search.v
+++ b/test-suite/output/Search.v
@@ -10,11 +10,19 @@ Search (@eq _ _ _) true -false "prop" -"intro".  (* andb_prop *)
 Definition newdef := fun x:nat => x.
 
 Goal forall n:nat, n <> newdef n -> newdef n <> n -> False.
-  intros n h h'.
+  cut False.
+  intros _ n h h'.
   Search n.                             (* search hypothesis *)
   Search newdef.                        (* search hypothesis *)
   Search ( _ <> newdef _).              (* search hypothesis, pattern *)
   Search ( _ <> newdef _) -"h'".        (* search hypothesis, pattern *)
+
+  1:Search newdef.
+  2:Search newdef.
+
+  Fail 3:Search newdef.
+  Fail 1-2:Search newdef.
+  Fail all:Search newdef.
 Abort.
 
 Goal forall n (P:nat -> Prop), P n -> ~P n -> False.