12 files changed, 147 insertions, 4 deletions
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index abc7f0f88e..e0aa758812 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -2,9 +2,9 @@ The command has indeed failed with message:
 Flag "rename" expected to rename A into B.
 File "stdin", line 3, characters 0-25:
 Warning: This command is just asserting the names of arguments of identity.
-If this is what you want add ': assert' to silence the warning. If you want
-to clear implicit arguments add ': clear implicits'. If you want to clear
-notation scopes add ': clear scopes' [arguments-assert,vernacular]
+If this is what you want, add ': assert' to silence the warning. If you want
+to clear implicit arguments, add ': clear implicits'. If you want to clear
+notation scopes, add ': clear scopes' [arguments-assert,vernacular]
 @eq_refl
      : forall (B : Type) (y : B), y = y
 eq_refl
diff --git a/test-suite/output/NotationsSigma.out b/test-suite/output/NotationsSigma.out
new file mode 100644
index 0000000000..0e4df87148
--- /dev/null
+++ b/test-suite/output/NotationsSigma.out
@@ -0,0 +1,40 @@
+{0 = 0} + {0 < 1}
+     : Set
+(0 = 0) + {0 < 1}
+     : Set
+{x : nat | x = 1}
+     : Set
+{x : nat | x = 1 & 0 < x}
+     : Set
+{x : nat | x = 1}
+     : Set
+{x : nat | x = 1 & 0 < x}
+     : Set
+{x : nat & x = 1}
+     : Set
+{x : nat & x = 1 & 0 < x}
+     : Set
+{x : nat & x = 1}
+     : Set
+{x : nat & x = 1 & 0 < x}
+     : Set
+{'(x, _) : nat * ?T | x = 1}
+     : Type
+where
+?T : [pat : nat * ?T |- Type] (pat cannot be used)
+{'(x, y) : nat * nat | x = 1 & y = 0}
+     : Set
+{'(x, _) : nat * nat | x = 1}
+     : Set
+{'(x, y) : nat * nat | x = 1 & y = 0}
+     : Set
+{'(x, _) : nat * ?T & x = 1}
+     : Type
+where
+?T : [pat : nat * ?T |- Type] (pat cannot be used)
+{'(x, y) : nat * nat & x = 1 & y = 0}
+     : Type
+{'(x, _) : nat * nat & x = 1}
+     : Type
+{'(x, y) : nat * nat & x = 1 & y = 0}
+     : Type
diff --git a/test-suite/output/NotationsSigma.v b/test-suite/output/NotationsSigma.v
new file mode 100644
index 0000000000..6780d63a04
--- /dev/null
+++ b/test-suite/output/NotationsSigma.v
@@ -0,0 +1,22 @@
+(* Check notations for sigma types *)
+
+Check { 0 = 0 } + { 0 < 1 }.
+Check (0 = 0) + { 0 < 1 }.
+
+Check { x | x = 1 }.
+Check { x | x = 1 & 0 < x }.
+Check { x : nat | x = 1 }.
+Check { x : nat | x = 1 & 0 < x }.
+Check { x & x = 1 }.
+Check { x & x = 1 & 0 < x }.
+Check { x : nat & x = 1 }.
+Check { x : nat & x = 1 & 0 < x }.
+
+Check {'(x,y) | x = 1 }.
+Check {'(x,y) | x = 1 & y = 0 }.
+Check {'(x,y) : nat * nat | x = 1 }.
+Check {'(x,y) : nat * nat | x = 1 & y = 0 }.
+Check {'(x,y) & x = 1 }.
+Check {'(x,y) & x = 1 & y = 0 }.
+Check {'(x,y) : nat * nat & x = 1 }.
+Check {'(x,y) : nat * nat & x = 1 & y = 0 }.
diff --git a/test-suite/output/Projections.out b/test-suite/output/Projections.out
index e9c28faf1d..1dd89c9bcd 100644
--- a/test-suite/output/Projections.out
+++ b/test-suite/output/Projections.out
@@ -1,2 +1,17 @@
 fun S : store => S.(store_funcs)
      : store -> host_func
+a = 
+fun A : Type =>
+let B := A in fun (C : Type) (u : U A C) => (A, B, C, c _ _ u)
+     : forall A : Type,
+       let B := A in
+       forall C : Type, U A C -> Type * Type * Type * (B * A * C)
+
+Arguments a (_ _)%type_scope
+b = 
+fun A : Type => let B := A in fun (C : Type) (u : U A C) => b _ _ u
+     : forall A : Type,
+       let B := A in
+       forall (C : Type) (u : U A C), (A, B, C, c _ _ u) = (A, B, C, c _ _ u)
+
+Arguments b (_ _)%type_scope
diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v
index 14d63d39c4..83a581338f 100644
--- a/test-suite/output/Projections.v
+++ b/test-suite/output/Projections.v
@@ -10,3 +10,12 @@ Section store.
 End store.
 
 Check (fun (S:@store nat) => S.(store_funcs)).
+
+Module LocalDefUnfolding.
+
+Unset Printing Projections.
+Record U A (B:=A) C := {c:B*A*C;a:=(A,B,C,c);b:a=a}.
+Print a.
+Print b.
+
+End LocalDefUnfolding.
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index 9d8e830d64..593d0c7f67 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -136,7 +136,7 @@ h': newdef n <> n
 (use "About" for full details on implicit arguments)
 (use "About" for full details on implicit arguments)
 The command has indeed failed with message:
-No such goal.
+[Focus] 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:
diff --git a/test-suite/output/UselessSyndef.out b/test-suite/output/UselessSyndef.out
new file mode 100644
index 0000000000..ce484889b3
--- /dev/null
+++ b/test-suite/output/UselessSyndef.out
@@ -0,0 +1,2 @@
+a
+     : nat
diff --git a/test-suite/output/UselessSyndef.v b/test-suite/output/UselessSyndef.v
new file mode 100644
index 0000000000..96ad6e9f5c
--- /dev/null
+++ b/test-suite/output/UselessSyndef.v
@@ -0,0 +1,10 @@
+Module M.
+  Definition a := 0.
+End M.
+Module N.
+  Notation a := M.a (only parsing).
+End N.
+
+Import M. Import N.
+
+Check a.
diff --git a/test-suite/output/bug_11934.out b/test-suite/output/bug_11934.out
new file mode 100644
index 0000000000..072136c82e
--- /dev/null
+++ b/test-suite/output/bug_11934.out
@@ -0,0 +1,13 @@
+thing = forall x y : foo, bla x y
+     : Prop
+thing = 
+forall (x : foo@{thing.u0}) (y : foo@{thing.u1}), bla x y
+     : Prop
+(* {thing.u1 thing.u0} |= bla.u0 = thing.u0
+                          bla.u1 = thing.u1 *)
+thing = 
+forall (x : @foo@{thing.u0} True) (y : @foo@{thing.u1} True),
+@bla True True x y
+     : Prop
+(* {thing.u1 thing.u0} |= bla.u0 = thing.u0
+                          bla.u1 = thing.u1 *)
diff --git a/test-suite/output/bug_11934.v b/test-suite/output/bug_11934.v
new file mode 100644
index 0000000000..fe9772dc62
--- /dev/null
+++ b/test-suite/output/bug_11934.v
@@ -0,0 +1,13 @@
+Polymorphic Axiom foo@{u} : Prop -> Prop.
+Arguments foo {_}.
+
+Axiom bla : forall {A B}, @foo A -> @foo B -> Prop.
+Definition thing := forall (x:@foo@{Type} True) (y:@foo@{Type} True), bla x y.
+
+Print thing. (* forall x y : foo, bla x y *)
+
+Set Printing Universes.
+Print thing. (* forall (x : foo@{thing.u0}) (y : foo@{thing.u1}), bla x y *)
+
+Set Printing Implicit.
+Print thing. (* BAD: forall x y : @foo@{thing.u0} True, @bla True True x y *)
diff --git a/test-suite/output/undeclared_key.out b/test-suite/output/undeclared_key.out
new file mode 100644
index 0000000000..ed768751fc
--- /dev/null
+++ b/test-suite/output/undeclared_key.out
@@ -0,0 +1,13 @@
+The command has indeed failed with message:
+There is no flag, option or table with this name: "Search Blacklists".
+The command has indeed failed with message:
+There is no qualid-valued table with this name: "Search Blacklist".
+File "stdin", line 3, characters 0-22:
+Warning: There is no flag or option with this name: "Search Blacklists".
+[unknown-option,option]
+The command has indeed failed with message:
+There is no string-valued table with this name: "Search Blacklists".
+The command has indeed failed with message:
+There is no qualid-valued table with this name: "Search Blacklist".
+The command has indeed failed with message:
+There is no qualid-valued table with this name: "Search Blacklist".
diff --git a/test-suite/output/undeclared_key.v b/test-suite/output/undeclared_key.v
new file mode 100644
index 0000000000..4134bc8bfa
--- /dev/null
+++ b/test-suite/output/undeclared_key.v
@@ -0,0 +1,6 @@
+Fail Test Search Blacklists.
+Fail Test Search Blacklist for foo.
+Set Search Blacklists.
+Fail Remove Search Blacklists "bar" foo.
+Fail Remove Search Blacklist "bar" foo.
+Fail Add Search Blacklist "bar" foo.