1 files changed, 36 insertions, 0 deletions
diff --git a/test-suite/success/Notations2.v b/test-suite/success/Notations2.v
index 9505a56e..7c2cf3ee 100644
--- a/test-suite/success/Notations2.v
+++ b/test-suite/success/Notations2.v
@@ -90,3 +90,39 @@ Check fun A (x :prod' bool A) => match x with #### 0 y 0 => 2 | _ => 1 end.
 Notation "##### x" := (pair' x) (at level 0, x at level 1).
 Check ##### 0 _ 0%bool 0%bool : prod' bool bool.
 Check fun A (x :prod' bool A) => match x with ##### 0 _ y 0%bool => 2 | _ => 1 end.
+
+(* 10. Check computation of binding variable through other notations *)
+(* it should be detected as binding variable and the scopes not being checked *)
+Notation "'FUNNAT' i => t" := (fun i : nat => i = t) (at level 200).
+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 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 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 *)
+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.