8 files changed, 104 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/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 *)