Merge PR #981: Miscellaneous fixes for notations

5 files changed, 21 insertions, 0 deletions

diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 9d106d2dac..7bcd7b041c 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -133,3 +133,5 @@ fun (x : nat) (p : x = x) => match p with
                              | 1 => 1
                              end = p
      : forall x : nat, x = x -> Prop
+bar  0
+     : nat
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index b9985a594f..fe6c05c39e 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -291,3 +291,11 @@ Check fun (x:nat) (p : x=x) => match p with ONE => ONE end = p.
 Notation "1" := eq_refl.
 Check fun (x:nat) (p : x=x) => match p with 1 => 1 end = p.
 
+(* Check bug 5693 *)
+
+Module M.
+Definition A := 0.
+Definition bar (a b : nat) := plus a b.
+Notation "" := A (format "", only printing).
+Check (bar A 0).
+End M.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index e5dbfcb4be..65efe228af 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -122,3 +122,5 @@ return (1, 2, 3, 4)
      : nat * nat * nat * nat
 {{ 1 | 1 // 1 }}
      : nat
+!!! _ _ : nat, True
+     : (nat -> Prop) * ((nat -> Prop) * Prop)
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index b1015137d6..ea372ad1a3 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -186,3 +186,7 @@ Check letpair x [1] = {0}; return (1,2,3,4).
 Notation "{ { xL | xR // xcut } }" := (xL+xR+xcut)
   (at level 0, xR at level 39, format "{ {  xL  |  xR  //  xcut  } }").
 Check 1+1+1.
+
+(* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *)
+Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder).
+Check !!! (x y:nat), True.
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 837f2efd06..4d04f2cf9b 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -142,3 +142,8 @@ Fail Notation "'foobarkeyword'" := (@nil) (only parsing, only printing).
 Reserved Notation "x === y" (at level 50).
 Inductive EQ {A} (x:A) : A -> Prop := REFL : x === x
  where "x === y" := (EQ x y).
+
+(* Check that strictly ident or _ are coerced to a name *)
+
+Fail Check {x@{u},y|x=x}.
+Fail Check {?[n],y|0=0}.