Suite picking numeral notation

Ceci est une suite à numeral notation in custom entries, cherchant à
raffiner la compatibilité entre entrées. C'est mélangé avec le "pick"
précédent, et c'est en chantier.

1 files changed, 14 insertions, 0 deletions

diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index 4ab800c9ba..dbfa939230 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -25,6 +25,20 @@ Check [ << # 0 >> ].
 Notation "n" := n%nat (in custom myconstr at level 0, n bigint).
 Check [ 2 + 3 ].
 
+Module A1.
+  (* This is compatible with bigint *)
+  Notation "x" := x (in custom myconstr at level 0, x ident).
+  (* This is incompatible with ident *)
+  Fail Notation "x" := x (in custom myconstr at level 0, x global).
+End A1.
+
+Module A2.
+  (* This is compatible with bigint *)
+  Notation "x" := x (in custom myconstr at level 0, x global).
+  (* This is compatible with bigint and global *)
+  Notation "x" := x (in custom myconstr at level 0, x string).
+End A2.
+
 End A.
 
 Module B.