Fixing a few other inconsistencies with notations.

`Notation ".a" := nat.' was accepted and used for printing but not
recognized in parsing. Now it does. Other examples in test-suite.

1 files changed, 29 insertions, 0 deletions

diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index 1d8278c08..ceb29d1b9 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -116,3 +116,32 @@ Check %j.
 
 Notation "{ x , y , .. , v }" := (fun a => (or .. (or (a = x) (a = y)) .. (a = v))).
 Check ({1, 2}).
+
+(**********************************************************************)
+(* Check notations of the form ".a", ".a≡", "a≡"                      *)
+(* Only "a#", "a≡" and ".≡" were working properly for parsing. The    *)
+(* other ones were working only for printing.                         *)
+
+Notation "a#" := nat.
+Check nat.
+Check a#.
+
+Notation "a≡" := nat.
+Check nat.
+Check a≡.
+
+Notation ".≡" := nat.
+Check nat.
+Check .≡.
+
+Notation ".a#" := nat.
+Check nat.
+Check .a#.
+
+Notation ".a≡" := nat.
+Check nat.
+Check .a≡.
+
+Notation ".α" := nat.
+Check nat.
+Check .α.