Notations: Adding modifiers to tell which kind of binder a constr can parse.

Concretely, we provide "constr as ident", "constr as strict pattern"
and "constr as pattern".

This tells to parse a binder as a constr, restricting to only ident or
to only a strict pattern, or to a pattern which can also be an ident.

The "strict pattern" modifier allows to restrict the use of patterns
in printing rules. This allows e.g. to select the appropriate rule for
printing between {x|P} and {'pat|P}.

3 files changed, 17 insertions, 6 deletions

diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index 6d195b5122..3fd4c1c311 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -194,8 +194,6 @@ pair
             (prod nat (prod nat nat))) (prod (prod nat nat) nat)
 fun x : nat => if x is n .+ 1 then n else 1
      : nat -> nat
-{{{x, y}} : nat * nat | x + y = 0}
-     : Set
 exists2' {{x, y}}, x = 0 & y = 0
      : Prop
 exists2 x : nat * nat,
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index b4ad4a7b3c..9ea218481e 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -341,8 +341,6 @@ Check fun x => if x is n.+1 then n else 1.
 
 (* Examples with binding patterns *)
 
-Check {(x,y)|x+y=0}.
-
 Module D.
 Notation "'exists2'' x , p & q" := (ex2 (fun x => p) (fun x => q))
   (at level 200, x pattern, p at level 200, right associativity,
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 08d904cea0..7c2cf3ee52 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -98,12 +98,12 @@ Notation "'Funnat' i => t" := (FUNNAT i => t + i%nat) (at level 200).
 
 (* 11. Notations with needed factorization of a recursive pattern *)
 (* See https://github.com/coq/coq/issues/6078#issuecomment-342287412 *)
-Module A.
+Module M11.
 Notation "[:: x1 ; .. ; xn & s ]" := (cons x1 .. (cons xn s) ..).
 Notation "[:: x1 ; .. ; xn ]" := (cons x1 .. (cons xn nil) ..).
 Check [:: 1 ; 2 ; 3 ].
 Check [:: 1 ; 2 ; 3 & nil ]. (* was failing *)
-End A.
+End M11.
 
 (* 12. Preventively check that a variable which does not occur can be instantiated *)
 (* by any term. In particular, it should not be restricted to a binder *)
@@ -111,3 +111,18 @@ Module M12.
 Notation "N ++ x" := (S x) (only parsing).
 Check 2 ++ 0.
 End M12.
+
+(* 13. Check that internal data about associativity are not used in comparing levels *)
+Module M13.
+Notation "x ;; z" := (x + z)
+  (at level 100, z at level 200, only parsing, right associativity).
+Notation "x ;; z" := (x * z)
+  (at level 100, z at level 200, only parsing) : foo_scope.
+End M13.
+
+(* 14. Check that a notation with a "ident" binder does not include a pattern *)
+Module M14.
+Notation "'myexists' x , p" := (ex (fun x => p))
+  (at level 200, x ident, p at level 200, right associativity) : type_scope.
+Check myexists I, I = 0. (* Should not be seen as a constructor *)
+End M14.