9 files changed, 59 insertions, 2 deletions
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 1987b6a6e9..304353f559 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -223,3 +223,11 @@ fun S : nat => [[S | S.S]]
      : Set
 exists2 '{{y, z}} : nat * nat, y > z & z > y
      : Prop
+foo = 
+fun l : list nat => match l with
+                    | _ :: (_ :: _) as l1 => l1
+                    | _ => l
+                    end
+     : list nat -> list nat
+
+Argument scope is [list_scope]
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index c165f9553e..d2d1369468 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -278,10 +278,12 @@ Set Printing Notations.
 
 (* Check insensitivity of "match" clauses to order *)
 
+Module IfPat.
 Notation "'if' t 'is' n .+ 1 'then' p 'else' q" :=
   (match t with S n => p | 0 => q end)
   (at level 200).
 Check fun x => if x is n.+1 then n else 1.
+End IfPat.
 
 (* Examples with binding patterns *)
 
@@ -338,11 +340,13 @@ Check ∀ '(((x,y),true)|((x,y),false)), x>y.
 
 (* Check Georges' printability of a "if is then else" notation *)
 
+Module IfPat2.
 Notation "'if' c 'is' p 'then' u 'else' v" :=
   (match c with p => u | _ => v end)
   (at level 200, p pattern at level 100).
 Check fun p => if p is S n then n else 0.
 Check fun p => if p is Lt then 1 else 0.
+End IfPat2.
 
 (* Check that mixed binders and terms defaults to ident and not pattern *)
 Module F.
@@ -364,3 +368,15 @@ Check {'(x,y)|x+y=0}.
 
 (* Check exists2 with a pattern *)
 Check ex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y).
+
+Module Issue7110.
+Open Scope list_scope.
+Notation "[ :: x1 , x2 , .. , xn & s ]" := (x1 :: x2 :: .. (xn :: s) ..)
+  (at level 0).
+Definition foo (l : list nat) :=
+  match l with
+  | a :: (b :: l) as l1 => l1
+  | _ => l
+end.
+Print foo.
+End Issue7110.
diff --git a/test-suite/output/Projections.out b/test-suite/output/Projections.out
new file mode 100644
index 0000000000..e9c28faf1d
--- /dev/null
+++ b/test-suite/output/Projections.out
@@ -0,0 +1,2 @@
+fun S : store => S.(store_funcs)
+     : store -> host_func
diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v
new file mode 100644
index 0000000000..098a518dc4
--- /dev/null
+++ b/test-suite/output/Projections.v
@@ -0,0 +1,11 @@
+
+Set Printing Projections.
+
+Class HostFunction := host_func : Type.
+
+Section store.
+  Context `{HostFunction}.
+  Record store := { store_funcs : host_func }.
+End store.
+
+Check (fun (S:@store nat) => S.(store_funcs)).
diff --git a/test-suite/output/bug5778.out b/test-suite/output/bug5778.out
index 91ceb1b583..d6056c5098 100644
--- a/test-suite/output/bug5778.out
+++ b/test-suite/output/bug5778.out
@@ -1,4 +1,4 @@
 The command has indeed failed with message:
-In nested Ltac calls to "c", "abs" and "abstract b ltac:(())", last call
-failed.
+In nested Ltac calls to "c", "abs", "abstract b ltac:(())", 
+"b", "a", "pose (I : I)" and "(I : I)", last term evaluation failed.
 The term "I" has type "True" which should be Set, Prop or Type.
diff --git a/test-suite/output/bug6404.out b/test-suite/output/bug6404.out
new file mode 100644
index 0000000000..05464755f0
--- /dev/null
+++ b/test-suite/output/bug6404.out
@@ -0,0 +1,4 @@
+The command has indeed failed with message:
+In nested Ltac calls to "c", "abs", "transparent_abstract (tactic3)", 
+"b", "a", "pose (I : I)" and "(I : I)", last term evaluation failed.
+The term "I" has type "True" which should be Set, Prop or Type.
diff --git a/test-suite/output/bug6404.v b/test-suite/output/bug6404.v
new file mode 100644
index 0000000000..bbe6b1a00f
--- /dev/null
+++ b/test-suite/output/bug6404.v
@@ -0,0 +1,7 @@
+Ltac a _ := pose (I : I).
+Ltac b _ := a ().
+Ltac abs _ := transparent_abstract b ().
+Ltac c _ := abs ().
+Goal True.
+  Fail c ().
+Abort.
diff --git a/test-suite/output/ssr_clear.out b/test-suite/output/ssr_clear.out
new file mode 100644
index 0000000000..1515954060
--- /dev/null
+++ b/test-suite/output/ssr_clear.out
@@ -0,0 +1,3 @@
+The command has indeed failed with message:
+Ltac call to "move (ssrmovearg) (ssrclauses)" failed.
+No assumption is named NO_SUCH_NAME
diff --git a/test-suite/output/ssr_clear.v b/test-suite/output/ssr_clear.v
new file mode 100644
index 0000000000..573ec47e0b
--- /dev/null
+++ b/test-suite/output/ssr_clear.v
@@ -0,0 +1,6 @@
+Require Import ssreflect.
+
+Example foo : True -> True.
+Proof.
+Fail move=> {NO_SUCH_NAME}.
+Abort.