Merge PR #13965: [abbreviation] user syntax to set interp scope of argument

Ack-by: JasonGross
Reviewed-by: herbelin
Reviewed-by: jashug
Reviewed-by: jfehrle
Reviewed-by: ppedrot

3 files changed, 44 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_3468.v b/test-suite/bugs/closed/bug_3468.v
index 6ff394bca6..8d7d97d7aa 100644
--- a/test-suite/bugs/closed/bug_3468.v
+++ b/test-suite/bugs/closed/bug_3468.v
@@ -26,4 +26,5 @@ Notation "& b" := ltac:(exact (b)%my) (at level 100, only parsing): my_scope.
 Definition test := (& (@4))%my.
 
 (* Check inconsistent scopes *)
+Set Warnings "+inconsistent-scopes".
 Fail Notation bar3 a := (let __ := ltac:(exact a%nat) in a%bool) (only parsing).
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).