7 files changed, 97 insertions, 1 deletions
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index caf3b28701..4740c009a4 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -163,6 +163,7 @@ match goal with |- ?y + _ = _ => pose (match y as y with 0 => 0 | S n => 0 end)
 match goal with |- ?y + _ = _ => pose (match y as y return y=y with 0 => eq_refl | S n => eq_refl end) end.
 match goal with |- ?y + _ = _ => pose (match y return y=y with 0 => eq_refl | S n => eq_refl end) end.
 Show.
+Abort.
 
 Lemma lem5 (p:nat) : eq_refl p = eq_refl p.
 let y := fresh "n" in (* Checking that y is hidden *)
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/UnclosedBlocks.out b/test-suite/output/UnclosedBlocks.out
index b83e94ad43..31481e84a5 100644
--- a/test-suite/output/UnclosedBlocks.out
+++ b/test-suite/output/UnclosedBlocks.out
@@ -1,3 +1,2 @@
-
 Error: The section Baz, module type Bar and module Foo need to be closed.
 
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 6adbe95dd5..901b1e3aa6 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -37,17 +37,20 @@ Fail g1 I.
 Fail f1 I.
 Fail g2 I.
 Fail f2 I.
+Abort.
 
 Ltac h x := injection x.
 Goal True -> False.
 Fail h I.
 intro H.
 Fail h H.
+Abort.
 
 (* Check printing of the "var" argument "Hx" *)
 Ltac m H := idtac H; exact H.
 Goal True.
 let a:=constr:(let Hx := 0 in ltac:(m Hx)) in idtac.
+Abort.
 
 (* Check consistency of interpretation scopes (#4398) *)
 
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.