Merge PR #11841: Distinguishing entry "ident" from entry "name" in term notations.

Reviewed-by: jfehrle
Reviewed-by: gares
Reviewed-by: Zimmi48
Reviewed-by: maximedenes

4 files changed, 7 insertions, 5 deletions

diff --git a/test-suite/bugs/closed/bug_9517.v b/test-suite/bugs/closed/bug_9517.v
index bb43edbe74..93ed94df39 100644
--- a/test-suite/bugs/closed/bug_9517.v
+++ b/test-suite/bugs/closed/bug_9517.v
@@ -2,6 +2,7 @@ Declare Custom Entry expr.
 Declare Custom Entry stmt.
 Notation "x" := x (in custom stmt, x ident).
 Notation "x" := x (in custom expr, x ident).
+Notation "'_'" := _ (in custom expr).
 
 Notation "1" := 1 (in custom expr).
 
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index bcb2468792..05712eaac7 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -62,7 +62,7 @@ Check `(∀ n p : A, n=p).
 
 Notation "'let'' f x .. y  :=  t 'in' u":=
   (let f := fun x => .. (fun y => t) .. in u)
-  (f ident, x closed binder, y closed binder, at level 200,
+  (f name, x closed binder, y closed binder, at level 200,
    right associativity).
 
 Check let' f x y (a:=0) z (b:bool) := x+y+z+1 in f 0 1 2.
@@ -93,7 +93,7 @@ End A.
 
 Notation "'mylet' f [ x ; .. ; y ]  :=  t 'in' u":=
   (let f := fun x => .. (fun y => t) .. in u)
-  (f ident, x closed binder, y closed binder, at level 200,
+  (f name, x closed binder, y closed binder, at level 200,
    right associativity).
 
 Check mylet f [x;y;z;(a:bool)] := x+y+z+1 in f 0 1 2.
@@ -104,7 +104,7 @@ Check mylet f [x;y;z;(a:bool)] := x+y+z+1 in f 0 1 2.
 (* Old request mentioned again on coq-club 20/1/2012 *)
 
 Notation "#  x : T => t" := (fun x : T => t)
-  (at level 0, t at level 200, x ident).
+  (at level 0, t at level 200, x name).
 
 Check # x : nat => x.
 Check # _ : nat => 2.
@@ -116,7 +116,7 @@ Parameters (A : Set) (x y : A) (Q : A -> A -> Prop) (conj : Q x y).
 Check (exist (Q x) y conj).
 
 (* Check bug #4854 *)
-Notation "% i" := (fun i : nat => i) (at level 0, i ident).
+Notation "% i" := (fun i : nat => i) (at level 0, i name).
 Check %i.
 Check %j.
 
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 04a91c14d9..6c714fc624 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -305,7 +305,7 @@ Module E.
 Inductive myex2 {A:Type} (P Q:A -> Prop) : Prop :=
   myex_intro2 : forall x:A, P x -> Q x -> myex2 P Q.
 Notation "'myexists2' x : A , p & q" := (myex2 (A:=A) (fun x => p) (fun x => q))
-  (at level 200, x ident, A at level 200, p at level 200, right associativity,
+  (at level 200, x name, A at level 200, p at level 200, right associativity,
     format "'[' 'myexists2'  '/  ' x  :  A ,  '/  ' '[' p  &  '/' q ']' ']'")
   : type_scope.
 Check myex2 (fun x => let '(y,z) := x in y>z) (fun x => let '(y,z) := x in z>y).
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index ebc1426fc8..ce488fe18d 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -327,6 +327,7 @@ Module P.
 
   Module NotationMixedTermBinderAsIdent.
 
+  Set Warnings "-deprecated-ident-entry". (* We do want ident! *)
   Notation "▢_ n P" := (pseudo_force n (fun n => P))
     (at level 0, n ident, P at level 9, format "▢_ n  P").
   Check exists p, ▢_p (p >= 1).