4 files changed, 93 insertions, 0 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 304353f559..996af59270 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -231,3 +231,13 @@ fun l : list nat => match l with
      : list nat -> list nat
 
 Argument scope is [list_scope]
+Notation
+"'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope
+(default interpretation)
+"'exists' ! x .. y , p" := ex
+                             (unique
+                                (fun x => .. (ex (unique (fun y => p))) ..))
+: type_scope (default interpretation)
+Notation
+"( x , y , .. , z )" := pair .. (pair x y) .. z : core_scope
+(default interpretation)
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index d2d1369468..3cf0c913f7 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -380,3 +380,8 @@ Definition foo (l : list nat) :=
 end.
 Print foo.
 End Issue7110.
+
+Module LocateNotations.
+Locate "exists".
+Locate "( _ , _ , .. , _ )".
+End LocateNotations.
diff --git a/test-suite/output/ssr_explain_match.out b/test-suite/output/ssr_explain_match.out
new file mode 100644
index 0000000000..fa2393b910
--- /dev/null
+++ b/test-suite/output/ssr_explain_match.out
@@ -0,0 +1,55 @@
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ - _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ <= _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ < _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ >= _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ > _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ <= _ <= _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ < _ <= _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ <= _ < _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ < _ < _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ + _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+File "stdin", line 12, characters 0-61:
+Warning: Notation _ * _ was already used in scope nat_scope.
+[notation-overridden,parsing]
+BEGIN INSTANCES
+instance: (x + y + z) matches: (x + y + z)
+instance: (x + y) matches: (x + y)
+instance: (x + y) matches: (x + y)
+END INSTANCES
+BEGIN INSTANCES
+instance: (addnC (x + y) z) matches: (x + y + z)
+instance: (addnC x y) matches: (x + y)
+instance: (addnC x y) matches: (x + y)
+END INSTANCES
+BEGIN INSTANCES
+instance: (addnA x y z) matches: (x + y + z)
+END INSTANCES
+BEGIN INSTANCES
+instance: (addnA x y z) matches: (x + y + z)
+instance: (addnC z (x + y)) matches: (x + y + z)
+instance: (addnC y x) matches: (x + y)
+instance: (addnC y x) matches: (x + y)
+END INSTANCES
+The command has indeed failed with message:
+Ltac call to "ssrinstancesoftpat (cpattern)" failed.
+Not supported
diff --git a/test-suite/output/ssr_explain_match.v b/test-suite/output/ssr_explain_match.v
new file mode 100644
index 0000000000..56ca24b6e2
--- /dev/null
+++ b/test-suite/output/ssr_explain_match.v
@@ -0,0 +1,23 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+Require Import ssrmatching.
+Require Import ssreflect ssrbool TestSuite.ssr_mini_mathcomp.
+
+Definition addnAC := (addnA, addnC).
+
+Lemma test x y z : x + y + z =  x + y.
+
+ssrinstancesoftpat (_ + _).
+ssrinstancesofruleL2R addnC.
+ssrinstancesofruleR2L addnA.
+ssrinstancesofruleR2L addnAC.
+Fail ssrinstancesoftpat (_ + _ in RHS). (* Not implemented *)
+Admitted.