4 files changed, 56 insertions, 0 deletions
diff --git a/test-suite/output/bug_13240.out b/test-suite/output/bug_13240.out
new file mode 100644
index 0000000000..5fccef5cfe
--- /dev/null
+++ b/test-suite/output/bug_13240.out
@@ -0,0 +1,3 @@
+Ltac t1 a b := a ; last  b
+Ltac t2 := do !idtac
+Ltac t3 := idtac => True
diff --git a/test-suite/output/bug_13240.v b/test-suite/output/bug_13240.v
new file mode 100644
index 0000000000..a999450cd2
--- /dev/null
+++ b/test-suite/output/bug_13240.v
@@ -0,0 +1,10 @@
+Require Import ssreflect.
+
+Ltac t1 a b := a; last b.
+Print t1.
+
+Ltac t2 := do !idtac.
+Print t2.
+
+Ltac t3 := idtac => True.
+Print t3.
diff --git a/test-suite/output/notation_principal_scope.out b/test-suite/output/notation_principal_scope.out
new file mode 100644
index 0000000000..5ccee259b0
--- /dev/null
+++ b/test-suite/output/notation_principal_scope.out
@@ -0,0 +1,20 @@
+The command has indeed failed with message:
+Argument X was previously inferred to be in scope function_scope but is here
+used in the empty scope stack. Scope function_scope will be used at parsing
+time unless you override it by annotating the argument with an explicit scope
+of choice. [inconsistent-scopes,syntax]
+The command has indeed failed with message:
+Simple notations don't support only printing
+The command has indeed failed with message:
+The reference nonexisting was not found in the current environment.
+The command has indeed failed with message:
+Notation scope for argument X can be specified only once.
+pp I
+     : True /\ True
+The command has indeed failed with message:
+Illegal application (Non-functional construction): 
+The expression "I" of type "True" cannot be applied to the term
+ "I" : "True"
+File "stdin", line 21, characters 0-50:
+Warning: This notation will not be used for printing as it is bound to a
+single variable. [notation-bound-to-variable,parsing]
diff --git a/test-suite/output/notation_principal_scope.v b/test-suite/output/notation_principal_scope.v
new file mode 100644
index 0000000000..6bd911501d
--- /dev/null
+++ b/test-suite/output/notation_principal_scope.v
@@ -0,0 +1,23 @@
+Arguments conj {_ _} _ _%function.
+
+Set Warnings "+inconsistent-scopes".
+Fail Notation pp X := (conj X X).
+
+Fail Notation pp := 1 (only printing).
+
+Fail Notation pp X := nonexisting.
+
+Fail Notation pp X := (conj X X) (X, X in scope nat_scope).
+
+Notation pp X := (conj X X) (X in scope nat_scope).
+
+Notation "$" := I (only parsing) : nat_scope.
+Notation "$" := (I I) (only parsing) : bool_scope.
+
+Open Scope bool_scope.
+Check pp $.
+Fail Check pp (id $).
+
+Notation pp1 X := (X%nat) (X in scope bool_scope).
+Notation pp2 X := ((X + X)%type) (X in scope bool_scope).
+Notation pp3 X := (((X, X)%type, X)%nat) (X in scope bool_scope).