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

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

25 files changed, 230 insertions, 92 deletions

diff --git a/doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst b/doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst
new file mode 100644
index 0000000000..8d681361e8
--- /dev/null
+++ b/doc/changelog/03-notations/11841-master+distinguishing-ident-name-in-grammar-entries.rst
@@ -0,0 +1,13 @@
+- **Changed:**
+  In notations (except in custom entries), the misleading :n:`@syntax_modifier`
+  :n:`@ident ident` (which accepted either an identifier or
+  a :g:`_`) is deprecated and should be replaced by :n:`@ident name`. If
+  the intent was really to only parse identifiers, this will
+  eventually become possible, but only as of Coq 8.15.
+  In custom entries, the meaning of :n:`@ident ident` is silently changed
+  from parsing identifiers or :g:`_` to parsing only identifiers
+  without warning, but this presumably affects only rare, recent and
+  relatively experimental code
+  (`#11841 <https://github.com/coq/coq/pull/11841>`_,
+  fixes `#9514 <https://github.com/coq/coq/pull/9514>`_,
+  by Hugo Herbelin).
diff --git a/doc/sphinx/language/extensions/canonical.rst b/doc/sphinx/language/extensions/canonical.rst
index f7ce7f1c6c..aa754ab63d 100644
--- a/doc/sphinx/language/extensions/canonical.rst
+++ b/doc/sphinx/language/extensions/canonical.rst
@@ -490,10 +490,10 @@ We need some infrastructure for that.
     Definition id {T} {t : T} (x : phantom t) := x.
 
     Notation "[find v | t1 ~ t2 ] p" := (fun v (_ : unify t1 t2 None) => p)
-      (at level 50, v ident, only parsing).
+      (at level 50, v name, only parsing).
 
     Notation "[find v | t1 ~ t2 | s ] p" := (fun v (_ : unify t1 t2 (Some s)) => p)
-      (at level 50, v ident, only parsing).
+      (at level 50, v name, only parsing).
 
     Notation "'Error : t : s" := (unify _ t (Some s))
       (at level 50, format "''Error' : t : s").
diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst
index 5cbd2e400e..df73de846f 100644
--- a/doc/sphinx/user-extensions/syntax-extensions.rst
+++ b/doc/sphinx/user-extensions/syntax-extensions.rst
@@ -603,7 +603,7 @@ Here is the basic example of a notation using a binder:
 .. coqtop:: in
 
    Notation "'sigma' x : A , B" := (sigT (fun x : A => B))
-     (at level 200, x ident, A at level 200, right associativity).
+     (at level 200, x name, A at level 200, right associativity).
 
 The binding variables in the right-hand side that occur as a parameter
 of the notation (here :g:`x`) dynamically bind all the occurrences
@@ -616,8 +616,9 @@ application of the notation:
 
    Check sigma z : nat, z = 0.
 
-Note the :n:`@syntax_modifier x ident` in the declaration of the
-notation. It tells to parse :g:`x` as a single identifier.
+Note the :n:`@syntax_modifier x name` in the declaration of the
+notation. It tells to parse :g:`x` as a single identifier (or as the
+unnamed variable :g:`_`).
 
 Binders bound in the notation and parsed as patterns
 ++++++++++++++++++++++++++++++++++++++++++++++++++++
@@ -655,7 +656,7 @@ variable. Here is an example showing the difference:
    Notation "'subset_bis' ' p , P" := (sig (fun p => P))
      (at level 200, p strict pattern).
    Notation "'subset_bis' p , P " := (sig (fun p => P))
-     (at level 200, p ident).
+     (at level 200, p name).
 
 .. coqtop:: all
 
@@ -675,18 +676,19 @@ the following:
 .. coqdoc::
 
    Notation "{ x : A | P }" := (sig (fun x : A => P))
-       (at level 0, x at level 99 as ident).
+       (at level 0, x at level 99 as name).
 
 This is so because the grammar also contains rules starting with :g:`{}` and
 followed by a term, such as the rule for the notation :g:`{ A } + { B }` for the
 constant :g:`sumbool` (see :ref:`specification`).
 
-Then, in the rule, ``x ident`` is replaced by ``x at level 99 as ident`` meaning
+Then, in the rule, ``x name`` is replaced by ``x at level 99 as name`` meaning
 that ``x`` is parsed as a term at level 99 (as done in the notation for
-:g:`sumbool`), but that this term has actually to be an identifier.
+:g:`sumbool`), but that this term has actually to be a name, i.e. an
+identifier or :g:`_`.
 
 The notation :g:`{ x | P }` is already defined in the standard
-library with the ``as ident`` :n:`@syntax_modifier`. We cannot redefine it but
+library with the ``as name`` :n:`@syntax_modifier`. We cannot redefine it but
 one can define an alternative notation, say :g:`{ p such that P }`,
 using instead ``as pattern``.
 
@@ -702,12 +704,12 @@ Then, the following works:
    Check {(x,y) such that x+y=0}.
 
 To enforce that the pattern should not be used for printing when it
-is just an identifier, one could have said
+is just a name, one could have said
 ``p at level 99 as strict pattern``.
 
-Note also that in the absence of a ``as ident``, ``as strict pattern`` or
+Note also that in the absence of a ``as name``, ``as strict pattern`` or
 ``as pattern`` :n:`@syntax_modifier`\s, the default is to consider sub-expressions occurring
-in binding position and parsed as terms to be ``as ident``.
+in binding position and parsed as terms to be ``as name``.
 
 Binders bound in the notation and parsed as general binders
 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
@@ -768,7 +770,7 @@ binding position. Here is an example:
 
    Definition force n (P:nat -> Prop) := forall n', n' >= n -> P n'.
    Notation "▢_ n P" := (force n (fun n => P))
-     (at level 0, n ident, P at level 9, format "▢_ n  P").
+     (at level 0, n name, P at level 9, format "▢_ n  P").
 
 .. coqtop:: all
 
@@ -946,16 +948,31 @@ position of :g:`x`:
      (at level 10, f global, a1, an at level 9).
 
 In addition to ``global``, one can restrict the syntax of a
-sub-expression by using the entry names ``ident`` or ``pattern``
+sub-expression by using the entry names ``ident``, ``name`` or ``pattern``
 already seen in :ref:`NotationsWithBinders`, even when the
 corresponding expression is not used as a binder in the right-hand
 side. E.g.:
 
+   .. todo: these two Set Warnings and the note should be removed when
+      ident is reactivated with its literal meaning.
+
+.. coqtop:: none
+
+   Set Warnings "-deprecated-ident-entry".
+
 .. coqtop:: in
 
    Notation "'apply_id' f a1 .. an" := (.. (f a1) .. an)
      (at level 10, f ident, a1, an at level 9).
 
+.. coqtop:: none
+
+   Set Warnings "+deprecated-ident-entry".
+
+.. note:: As of version 8.13, the entry ``ident`` is a deprecated
+          alias for ``name``. In the future, it is planned to strictly
+          parse an identifier (excluding :g:`_`).
+
 .. _custom-entries:
 
 Custom entries
@@ -1113,6 +1130,31 @@ gives a way to let any arbitrary expression which is not handled by the
 custom entry ``expr`` be parsed or printed by the main grammar of term
 up to the insertion of a pair of curly brackets.
 
+Another special situation is when parsing global references or
+identifiers. To indicate that a custom entry should parse identifiers,
+use the following form:
+
+.. coqtop:: none
+
+   Reset Initial.
+   Declare Custom Entry expr.
+
+.. coqtop:: in
+
+   Notation "x" := x (in custom expr at level 0, x ident).
+
+Similarly, to indicate that a custom entry should parse global references
+(i.e. qualified or non qualified identifiers), use the following form:
+
+.. coqtop:: none
+
+   Reset Initial.
+   Declare Custom Entry expr.
+
+.. coqtop:: in
+
+   Notation "x" := x (in custom expr at level 0, x global).
+
 .. cmd:: Print Custom Grammar @ident
    :name: Print Custom Grammar
 
@@ -1142,6 +1184,7 @@ Here are the syntax elements used by the various notation commands.
       | only printing
       | format @string {? @string }
       explicit_subentry ::= ident
+      | name
       | global
       | bigint
       | strict pattern {? at level @natural }
@@ -1151,6 +1194,7 @@ Here are the syntax elements used by the various notation commands.
       | custom @ident {? at @level } {? @binder_interp }
       | pattern {? at level @natural }
       binder_interp ::= as ident
+      | as name
       | as pattern
       | as strict pattern
       level ::= level @natural
@@ -1188,6 +1232,27 @@ Here are the syntax elements used by the various notation commands.
              due to legacy notation in the Coq standard library.
              It can be turned on with the ``-w disj-pattern-notation`` flag.
 
+.. note::
+
+   As of version 8.13, the entry ``ident`` is a deprecated alias for
+   ``name``. In the future, it is planned to strictly parse an
+   identifier (to the exclusion of :g:`_`). If the intent was to use
+   ``ident`` as an identifier (excluding :g:`_`), just silence the warning with
+   :n:`Set Warnings "-deprecated-ident-entry"` and it should automatically
+   get its intended meaning in version 8.15.
+
+   Similarly, ``as ident`` is a deprecated alias for ``as name``, which
+   will only accept an identifier in the future.  If the
+   intent was to use ``as ident`` as an identifier
+   (excluding :g:`_`), just silence the warning with
+   :n:`Set Warnings "-deprecated-as-ident-kind"`.
+
+   However, this deprecation does not apply to custom entries, where it
+   already denotes an identifier, as expected.
+
+   .. todo: the note above should be removed at the end of deprecation
+      phase of ident
+   ..
 .. _Scopes:
 
 Notation scopes
diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
index cdee623850..d01f66c6d7 100644
--- a/doc/tools/docgram/fullGrammar
+++ b/doc/tools/docgram/fullGrammar
@@ -1420,6 +1420,7 @@ syntax_modifiers: [
 
 explicit_subentry: [
 | "ident"
+| "name"
 | "global"
 | "bigint"
 | "binder"
@@ -1440,6 +1441,7 @@ at_level_opt: [
 
 binder_interp: [
 | "as" "ident"
+| "as" "name"
 | "as" "pattern"
 | "as" "strict" "pattern"
 ]
diff --git a/doc/tools/docgram/orderedGrammar b/doc/tools/docgram/orderedGrammar
index c27169d432..f62dd8f731 100644
--- a/doc/tools/docgram/orderedGrammar
+++ b/doc/tools/docgram/orderedGrammar
@@ -1579,6 +1579,7 @@ syntax_modifier: [
 
 explicit_subentry: [
 | "ident"
+| "name"
 | "global"
 | "bigint"
 | "strict" "pattern" OPT ( "at" "level" natural )
@@ -1591,6 +1592,7 @@ explicit_subentry: [
 
 binder_interp: [
 | "as" "ident"
+| "as" "name"
 | "as" "pattern"
 | "as" "strict" "pattern"
 ]
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8bd77abc4a..0645636255 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -976,6 +976,9 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c =
    into a substitution for interpretation and based on binding/constr
    distinction *)
 
+let cases_pattern_of_id {loc;v=id} =
+  CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
+
 let cases_pattern_of_name {loc;v=na} =
   let atom = match na with Name id -> Some (qualid_of_ident ?loc id) | Anonymous -> None in
   CAst.make ?loc (CPatAtom atom)
@@ -991,16 +994,20 @@ let split_by_type ids subst =
     | NtnTypeConstr ->
        let terms,terms' = bind id scl terms terms' in
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
-    | NtnTypeBinder NtnBinderParsedAsConstr (AsIdentOrPattern | AsStrictPattern) ->
+    | NtnTypeBinder NtnBinderParsedAsConstr (AsNameOrPattern | AsStrictPattern) ->
        let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
        let binders' = Id.Map.add id ((coerce_to_cases_pattern_expr a,Explicit),(false,scl)) binders' in
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
     | NtnTypeBinder NtnBinderParsedAsConstr AsIdent ->
        let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
+       let binders' = Id.Map.add id ((cases_pattern_of_id (coerce_to_id a),Explicit),(true,scl)) binders' in
+       (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
+    | NtnTypeBinder NtnBinderParsedAsConstr AsName ->
+       let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
        let binders' = Id.Map.add id ((cases_pattern_of_name (coerce_to_name a),Explicit),(true,scl)) binders' in
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
-    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnParsedAsBinder as x) ->
-       let onlyident = (x = NtnParsedAsIdent) in
+    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsName | NtnParsedAsPattern _ | NtnParsedAsBinder as x) ->
+       let onlyident = (x = NtnParsedAsIdent || x = NtnParsedAsName) in
        let binders,binders' = bind id (onlyident,scl) binders binders' in
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
     | NtnTypeConstrList ->
diff --git a/interp/notation.ml b/interp/notation.ml
index b5951a9c59..c35ba44aa5 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -62,10 +62,11 @@ let pair_eq f g (x1, y1) (x2, y2) = f x1 x2 && g y1 y2
 
 let notation_binder_source_eq s1 s2 = match s1, s2 with
 | NtnParsedAsIdent,  NtnParsedAsIdent -> true
+| NtnParsedAsName,  NtnParsedAsName -> true
 | NtnParsedAsPattern b1, NtnParsedAsPattern b2 -> b1 = b2
 | NtnBinderParsedAsConstr bk1, NtnBinderParsedAsConstr bk2 -> bk1 = bk2
 | NtnParsedAsBinder,  NtnParsedAsBinder -> true
-| (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _ | NtnParsedAsBinder), _ -> false
+| (NtnParsedAsIdent | NtnParsedAsName | NtnParsedAsPattern _ | NtnBinderParsedAsConstr _ | NtnParsedAsBinder), _ -> false
 
 let ntpe_eq t1 t2 = match t1, t2 with
 | NtnTypeConstr, NtnTypeConstr -> true
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index f51d3bfdfb..036970ce37 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -881,7 +881,7 @@ let is_onlybinding_meta id metas =
 let is_onlybinding_pattern_like_meta isvar id metas =
   try match Id.List.assoc id metas with
       | _,NtnTypeBinder (NtnBinderParsedAsConstr
-                           (AsIdentOrPattern | AsStrictPattern)) -> true
+                           (AsNameOrPattern | AsStrictPattern)) -> true
       | _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar)
       | _,NtnTypeBinder NtnParsedAsBinder -> not isvar
       | _ -> false
@@ -1533,7 +1533,7 @@ let match_notation_constr ~print_univ c ~vars (metas,pat) =
           let v = glob_constr_of_cases_pattern (Global.env()) pat in
           (((vars,v),scl)::terms',termlists',binders',binderlists')
         | _ -> raise No_match)
-    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsPattern _ | NtnParsedAsBinder) ->
+    | NtnTypeBinder (NtnParsedAsIdent | NtnParsedAsName | NtnParsedAsPattern _ | NtnParsedAsBinder) ->
        (terms',termlists',(Id.List.assoc x binders,scl)::binders',binderlists')
     | NtnTypeConstrList ->
        (terms',(Id.List.assoc x termlists,scl)::termlists',binders',binderlists')
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 29db23cc54..c541a19bfd 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -67,7 +67,8 @@ type extended_subscopes = Constrexpr.notation_entry_level * subscopes
 
 type constr_as_binder_kind =
   | AsIdent
-  | AsIdentOrPattern
+  | AsName
+  | AsNameOrPattern
   | AsStrictPattern
 
 type notation_binder_source =
@@ -76,6 +77,8 @@ type notation_binder_source =
   | NtnParsedAsPattern of bool
   (* This accepts only ident *)
   | NtnParsedAsIdent
+  (* This accepts only name *)
+  | NtnParsedAsName
   (* This accepts ident, or pattern, or both *)
   | NtnBinderParsedAsConstr of constr_as_binder_kind
   (* This accepts ident, _, and quoted pattern *)
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 94c3768116..7d2ed9aed0 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -32,6 +32,7 @@ let production_level_eq lev1 lev2 =
 
 type 'a constr_entry_key_gen =
   | ETIdent
+  | ETName of bool (* Temporary: true = user told "name", false = user wrote "ident" *)
   | ETGlobal
   | ETBigint
   | ETBinder of bool  (* open list of binders if true, closed list of binders otherwise *)
@@ -55,6 +56,7 @@ type binder_entry_kind = ETBinderOpen | ETBinderClosed of string Tok.p list
 type binder_target = ForBinder | ForTerm
 
 type constr_prod_entry_key =
+  | ETProdIdent           (* Parsed as an ident *)
   | ETProdName            (* Parsed as a name (ident or _) *)
   | ETProdReference       (* Parsed as a global reference *)
   | ETProdBigint          (* Parsed as an (unbounded) integer *)
diff --git a/parsing/extend.mli b/parsing/extend.mli
index b698415fd6..3cea45c3f5 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -27,6 +27,7 @@ val production_level_eq : production_level -> production_level -> bool
 
 type 'a constr_entry_key_gen =
   | ETIdent
+  | ETName of bool (* Temporary: true = user told "name", false = user wrote "ident" *)
   | ETGlobal
   | ETBigint
   | ETBinder of bool  (* open list of binders if true, closed list of binders otherwise *)
@@ -50,6 +51,7 @@ type binder_entry_kind = ETBinderOpen | ETBinderClosed of string Tok.p list
 type binder_target = ForBinder | ForTerm
 
 type constr_prod_entry_key =
+  | ETProdIdent           (* Parsed as an ident *)
   | ETProdName            (* Parsed as a name (ident or _) *)
   | ETProdReference       (* Parsed as a global reference *)
   | ETProdBigint          (* Parsed as an (unbounded) integer *)
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).
diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index 023705e169..5247c7b56a 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -309,9 +309,9 @@ Notation "'exists' x .. y , p" := (ex (fun x => .. (ex (fun y => p)) ..))
   : type_scope.
 
 Notation "'exists2' x , p & q" := (ex2 (fun x => p) (fun x => q))
-  (at level 200, x ident, p at level 200, right associativity) : type_scope.
+  (at level 200, x name, p at level 200, right associativity) : type_scope.
 Notation "'exists2' x : A , p & q" := (ex2 (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 "'[' 'exists2'  '/  ' x  :  A ,  '/  ' '[' p  &  '/' q ']' ']'")
   : type_scope.
 
@@ -489,18 +489,18 @@ Module EqNotations.
     := (match H as p in (_ = y) return P with
         | eq_refl => H'
         end)
-         (at level 10, H' at level 10, y ident, p ident,
+         (at level 10, H' at level 10, y name, p name,
           format "'[' 'rew'  'dependent'  [ 'fun'  y  p  =>  P ]  '/    ' H  in  '/' H' ']'").
   Notation "'rew' 'dependent' -> [ 'fun' y p => P ] H 'in' H'"
     := (match H as p in (_ = y) return P with
         | eq_refl => H'
         end)
-         (at level 10, H' at level 10, y ident, p ident, only parsing).
+         (at level 10, H' at level 10, y name, p name, only parsing).
   Notation "'rew' 'dependent' <- [ 'fun' y p => P ] H 'in' H'"
     := (match eq_sym H as p in (_ = y) return P with
         | eq_refl => H'
         end)
-         (at level 10, H' at level 10, y ident, p ident,
+         (at level 10, H' at level 10, y name, p name,
           format "'[' 'rew'  'dependent'  <-  [ 'fun'  y  p  =>  P ]  '/    ' H  in  '/' H' ']'").
   Notation "'rew' 'dependent' [ P ] H 'in' H'"
     := (match H as p in (_ = y) return P y p with
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index 84d40035bf..1a2c4ba171 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -96,19 +96,19 @@ Module Generic.
 (* begin hide *)
 (* Notations used in the proof. Hidden in coqdoc. *)
 
-Reserved Notation "'∀₁' x : A , B" (at level 200, x ident, A at level 200,right associativity).
+Reserved Notation "'∀₁' x : A , B" (at level 200, x name, A at level 200,right associativity).
 Reserved Notation "A '⟶₁' B" (at level 99, right associativity, B at level 200).
-Reserved Notation "'λ₁' x , u" (at level 200, x ident, right associativity).
+Reserved Notation "'λ₁' x , u" (at level 200, x name, right associativity).
 Reserved Notation "f '·₁' x" (at level 5, left associativity).
-Reserved Notation "'∀₂' A , F" (at level 200, A ident, right associativity).
-Reserved Notation "'λ₂' x , u" (at level 200, x ident, right associativity).
+Reserved Notation "'∀₂' A , F" (at level 200, A name, right associativity).
+Reserved Notation "'λ₂' x , u" (at level 200, x name, right associativity).
 Reserved Notation "f '·₁' [ A ]" (at level 5, left associativity).
-Reserved Notation "'∀₀' x : A , B" (at level 200, x ident, A at level 200,right associativity).
+Reserved Notation "'∀₀' x : A , B" (at level 200, x name, A at level 200,right associativity).
 Reserved Notation "A '⟶₀' B" (at level 99, right associativity, B at level 200).
-Reserved Notation "'λ₀' x , u" (at level 200, x ident, right associativity).
+Reserved Notation "'λ₀' x , u" (at level 200, x name, right associativity).
 Reserved Notation "f '·₀' x" (at level 5, left associativity).
-Reserved Notation "'∀₀¹' A : U , F" (at level 200, A ident, right associativity).
-Reserved Notation "'λ₀¹' x , u" (at level 200, x ident, right associativity).
+Reserved Notation "'∀₀¹' A : U , F" (at level 200, A name, right associativity).
+Reserved Notation "'λ₀¹' x , u" (at level 200, x name, right associativity).
 Reserved Notation "f '·₀' [ A ]" (at level 5, left associativity).
 
 (* end hide *)
diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index 9c8508bf39..b2bdd8099a 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -18,7 +18,7 @@ Set Implicit Arguments.
 
 Notation "{ ( x , y )  :  A  |  P }" :=
   (sig (fun anonymous : A => let (x,y) := anonymous in P))
-  (x ident, y ident, at level 10) : type_scope.
+  (x name, y name, at level 10) : type_scope.
 
 Declare Scope program_scope.
 Delimit Scope program_scope with prg.
diff --git a/theories/ssr/ssrbool.v b/theories/ssr/ssrbool.v
index d1cefeb552..a563dcbf95 100644
--- a/theories/ssr/ssrbool.v
+++ b/theories/ssr/ssrbool.v
@@ -335,19 +335,19 @@ Reserved Notation "[ 'predType' 'of' T ]" (at level 0,
 
 Reserved Notation "[ 'pred' : T | E ]" (at level 0,
   format "'[hv' [ 'pred' :  T  | '/ '  E ] ']'").
-Reserved Notation "[ 'pred' x | E ]" (at level 0, x ident,
+Reserved Notation "[ 'pred' x | E ]" (at level 0, x name,
   format "'[hv' [ 'pred'  x  | '/ '  E ] ']'").
-Reserved Notation "[ 'pred' x : T | E ]" (at level 0, x ident,
+Reserved Notation "[ 'pred' x : T | E ]" (at level 0, x name,
   format "'[hv' [ 'pred'  x  :  T  | '/ '  E ] ']'").
-Reserved Notation "[ 'pred' x | E1 & E2 ]" (at level 0, x ident,
+Reserved Notation "[ 'pred' x | E1 & E2 ]" (at level 0, x name,
   format "'[hv' [ 'pred'  x  | '/ '  E1  & '/ '  E2 ] ']'").
-Reserved Notation "[ 'pred' x : T | E1 & E2 ]" (at level 0, x ident,
+Reserved Notation "[ 'pred' x : T | E1 & E2 ]" (at level 0, x name,
   format "'[hv' [ 'pred'  x  :  T  | '/ '  E1  &  E2 ] ']'").
-Reserved Notation "[ 'pred' x 'in' A ]" (at level 0, x ident,
+Reserved Notation "[ 'pred' x 'in' A ]" (at level 0, x name,
   format "'[hv' [ 'pred'  x  'in'  A ] ']'").
-Reserved Notation "[ 'pred' x 'in' A | E ]" (at level 0, x ident,
+Reserved Notation "[ 'pred' x 'in' A | E ]" (at level 0, x name,
   format "'[hv' [ 'pred'  x  'in'  A  | '/ '  E ] ']'").
-Reserved Notation "[ 'pred' x 'in' A | E1 & E2 ]" (at level 0, x ident,
+Reserved Notation "[ 'pred' x 'in' A | E1 & E2 ]" (at level 0, x name,
   format "'[hv' [ 'pred'  x  'in'  A  | '/ '  E1  & '/ '  E2 ] ']'").
 
 Reserved Notation "[ 'qualify' x | P ]" (at level 0, x at level 99,
@@ -363,17 +363,17 @@ Reserved Notation "[ 'qualify' 'an' x | P ]" (at level 0, x at level 99,
 Reserved Notation "[ 'qualify' 'an' x : T | P ]" (at level 0, x at level 99,
   format "'[hv' [ 'qualify'  'an'  x  :  T  | '/ '  P ] ']'").
 
-Reserved Notation "[ 'rel' x y | E ]"  (at level 0, x ident, y ident,
+Reserved Notation "[ 'rel' x y | E ]"  (at level 0, x name, y name,
   format "'[hv' [ 'rel'  x  y  | '/ '  E ] ']'").
-Reserved Notation "[ 'rel' x y : T | E ]" (at level 0, x ident, y ident,
+Reserved Notation "[ 'rel' x y : T | E ]" (at level 0, x name, y name,
   format "'[hv' [ 'rel'  x  y  :  T  | '/ '  E ] ']'").
-Reserved Notation "[ 'rel' x y 'in' A & B | E ]" (at level 0, x ident, y ident,
+Reserved Notation "[ 'rel' x y 'in' A & B | E ]" (at level 0, x name, y name,
   format "'[hv' [ 'rel'  x  y  'in'  A  &  B  | '/ '  E ] ']'").
-Reserved Notation "[ 'rel' x y 'in' A & B ]" (at level 0, x ident, y ident,
+Reserved Notation "[ 'rel' x y 'in' A & B ]" (at level 0, x name, y name,
   format "'[hv' [ 'rel'  x  y  'in'  A  &  B ] ']'").
-Reserved Notation "[ 'rel' x y 'in' A | E ]" (at level 0, x ident, y ident,
+Reserved Notation "[ 'rel' x y 'in' A | E ]" (at level 0, x name, y name,
   format "'[hv' [ 'rel'  x  y  'in'  A  | '/ '  E ] ']'").
-Reserved Notation "[ 'rel' x y 'in' A ]" (at level 0, x ident, y ident,
+Reserved Notation "[ 'rel' x y 'in' A ]" (at level 0, x name, y name,
   format "'[hv' [ 'rel'  x  y  'in'  A ] ']'").
 
 Reserved Notation "[ 'mem' A ]" (at level 0, format "[ 'mem'  A ]").
diff --git a/theories/ssr/ssreflect.v b/theories/ssr/ssreflect.v
index d0508bef2e..dc81b5cca7 100644
--- a/theories/ssr/ssreflect.v
+++ b/theories/ssr/ssreflect.v
@@ -110,7 +110,7 @@ Reserved Notation "'if' c 'then' vT 'else' vF" (at level 200,
 Reserved Notation "'if' c 'return' R 'then' vT 'else' vF" (at level 200,
   c, R, vT, vF at level 200).
 Reserved Notation "'if' c 'as' x 'return' R 'then' vT 'else' vF" (at level 200,
-  c, R, vT, vF at level 200, x ident).
+  c, R, vT, vF at level 200, x name).
 
 Reserved Notation "x : T" (at level 100, right associativity,
   format "'[hv' x '/ '  :  T ']'").
diff --git a/theories/ssr/ssrfun.v b/theories/ssr/ssrfun.v
index e1442e1da2..ba66e04e4a 100644
--- a/theories/ssr/ssrfun.v
+++ b/theories/ssr/ssrfun.v
@@ -236,19 +236,19 @@ Reserved Notation "'fun' => E" (at level 200, format "'fun' =>  E").
 Reserved Notation "[ 'fun' : T => E ]" (at level 0,
   format "'[hv' [ 'fun' :  T  => '/ '  E ] ']'").
 Reserved Notation "[ 'fun' x => E ]" (at level 0,
-  x ident, format "'[hv' [ 'fun'  x  => '/ '  E ] ']'").
+  x name, format "'[hv' [ 'fun'  x  => '/ '  E ] ']'").
 Reserved Notation "[ 'fun' x : T => E ]" (at level 0,
-  x ident, format "'[hv' [ 'fun'  x  :  T  => '/ '  E ] ']'").
+  x name, format "'[hv' [ 'fun'  x  :  T  => '/ '  E ] ']'").
 Reserved Notation "[ 'fun' x y => E ]" (at level 0,
-  x ident, y ident, format "'[hv' [ 'fun'  x  y  => '/ '  E ] ']'").
+  x name, y name, format "'[hv' [ 'fun'  x  y  => '/ '  E ] ']'").
 Reserved Notation "[ 'fun' x y : T => E ]" (at level 0,
-  x ident, y ident, format "'[hv' [ 'fun'  x  y  :  T  => '/ '  E ] ']'").
+  x name, y name, format "'[hv' [ 'fun'  x  y  :  T  => '/ '  E ] ']'").
 Reserved Notation "[ 'fun' ( x : T ) y => E ]" (at level 0,
-  x ident, y ident, format "'[hv' [ 'fun'  ( x  :  T )  y  => '/ '  E ] ']'").
+  x name, y name, format "'[hv' [ 'fun'  ( x  :  T )  y  => '/ '  E ] ']'").
 Reserved Notation "[ 'fun' x ( y : T ) => E ]" (at level 0,
-  x ident, y ident, format "'[hv' [ 'fun'  x  ( y  :  T )  => '/ '  E ] ']'").
+  x name, y name, format "'[hv' [ 'fun'  x  ( y  :  T )  => '/ '  E ] ']'").
 Reserved Notation "[ 'fun' ( x : T ) ( y : U ) => E ]" (at level 0,
-  x ident, y ident, format "[ 'fun'  ( x  :  T )  ( y  :  U )  =>  E ]" ).
+  x name, y name, format "[ 'fun'  ( x  :  T )  ( y  :  U )  =>  E ]" ).
 
 Reserved Notation "f =1 g" (at level 70, no associativity).
 Reserved Notation "f =1 g :> A" (at level 70, g at next level, A at level 90).
@@ -259,33 +259,33 @@ Reserved Notation "f \; g" (at level 60, right associativity,
   format "f  \; '/ '  g").
 
 Reserved Notation "{ 'morph' f : x / a >-> r }" (at level 0, f at level 99,
-  x ident, format "{ 'morph'  f  :  x  /  a  >->  r }").
+  x name, format "{ 'morph'  f  :  x  /  a  >->  r }").
 Reserved Notation "{ 'morph' f : x / a }" (at level 0, f at level 99,
-  x ident, format "{ 'morph'  f  :  x  /  a }").
+  x name, format "{ 'morph'  f  :  x  /  a }").
 Reserved Notation "{ 'morph' f : x y / a >-> r }" (at level 0, f at level 99,
-  x ident, y ident, format "{ 'morph'  f  :  x  y  /  a  >->  r }").
+  x name, y name, format "{ 'morph'  f  :  x  y  /  a  >->  r }").
 Reserved Notation "{ 'morph' f : x y / a }" (at level 0, f at level 99,
-  x ident, y ident, format "{ 'morph'  f  :  x  y  /  a }").
+  x name, y name, format "{ 'morph'  f  :  x  y  /  a }").
 Reserved Notation "{ 'homo' f : x / a >-> r }" (at level 0, f at level 99,
-  x ident, format "{ 'homo'  f  :  x  /  a  >->  r }").
+  x name, format "{ 'homo'  f  :  x  /  a  >->  r }").
 Reserved Notation "{ 'homo' f : x / a }"  (at level 0, f at level 99,
-  x ident, format "{ 'homo'  f  :  x  /  a }").
+  x name, format "{ 'homo'  f  :  x  /  a }").
 Reserved Notation "{ 'homo' f : x y / a >-> r }" (at level 0, f at level 99,
-  x ident, y ident, format "{ 'homo'  f  :  x  y  /  a  >->  r }").
+  x name, y name, format "{ 'homo'  f  :  x  y  /  a  >->  r }").
 Reserved Notation "{ 'homo' f : x y / a }" (at level 0, f at level 99,
-  x ident, y ident, format "{ 'homo'  f  :  x  y  /  a }").
+  x name, y name, format "{ 'homo'  f  :  x  y  /  a }").
 Reserved Notation "{ 'homo' f : x y /~ a }" (at level 0, f at level 99,
-  x ident, y ident, format "{ 'homo'  f  :  x  y  /~  a }").
+  x name, y name, format "{ 'homo'  f  :  x  y  /~  a }").
 Reserved Notation "{ 'mono' f : x / a >-> r }" (at level 0, f at level 99,
-  x ident, format "{ 'mono'  f  :  x  /  a  >->  r }").
+  x name, format "{ 'mono'  f  :  x  /  a  >->  r }").
 Reserved Notation "{ 'mono' f : x / a }" (at level 0, f at level 99,
-  x ident, format "{ 'mono'  f  :  x  /  a }").
+  x name, format "{ 'mono'  f  :  x  /  a }").
 Reserved Notation "{ 'mono' f : x y / a >-> r }" (at level 0, f at level 99,
-  x ident, y ident, format "{ 'mono'  f  :  x  y  /  a  >->  r }").
+  x name, y name, format "{ 'mono'  f  :  x  y  /  a  >->  r }").
 Reserved Notation "{ 'mono' f : x y / a }" (at level 0, f at level 99,
-  x ident, y ident, format "{ 'mono'  f  :  x  y  /  a }").
+  x name, y name, format "{ 'mono'  f  :  x  y  /  a }").
 Reserved Notation "{ 'mono' f : x y /~ a }" (at level 0, f at level 99,
-  x ident, y ident, format "{ 'mono'  f  :  x  y  /~  a }").
+  x name, y name, format "{ 'mono'  f  :  x  y  /~  a }").
 
 Reserved Notation "@ 'id' T" (at level 10, T at level 8, format "@ 'id'  T").
 Reserved Notation "@ 'sval'" (at level 10, format "@ 'sval'").
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index ad6ac8d3f3..9fe3e2f7ab 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -246,6 +246,7 @@ type _ target =
 type prod_info = production_level * production_position
 
 type (_, _) entry =
+| TTIdent : ('self, lident) entry
 | TTName : ('self, lname) entry
 | TTReference : ('self, qualid) entry
 | TTBigint : ('self, string) entry
@@ -364,6 +365,7 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol =
 | TTPattern p -> MayRecNo (Pcoq.Symbol.nterml Constr.pattern (string_of_int p))
 | TTClosedBinderList [] -> MayRecNo (Pcoq.Symbol.list1 (Pcoq.Symbol.nterm Constr.binder))
 | TTClosedBinderList tkl -> MayRecNo (Pcoq.Symbol.list1sep (Pcoq.Symbol.nterm Constr.binder) (make_sep_rules tkl) false)
+| TTIdent -> MayRecNo (Pcoq.Symbol.nterm Prim.identref)
 | TTName -> MayRecNo (Pcoq.Symbol.nterm Prim.name)
 | TTBinder true -> MayRecNo (Pcoq.Symbol.nterm Constr.one_open_binder)
 | TTBinder false -> MayRecNo (Pcoq.Symbol.nterm Constr.one_closed_binder)
@@ -372,6 +374,7 @@ let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol =
 | TTReference -> MayRecNo (Pcoq.Symbol.nterm Constr.global)
 
 let interp_entry forpat e = match e with
+| ETProdIdent -> TTAny TTIdent
 | ETProdName -> TTAny TTName
 | ETProdReference -> TTAny TTReference
 | ETProdBigint -> TTAny TTBigint
@@ -382,6 +385,9 @@ let interp_entry forpat e = match e with
 | ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList
 | ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl)
 
+let cases_pattern_expr_of_id { CAst.loc; v = id } =
+  CAst.make ?loc @@ CPatAtom (Some (qualid_of_ident ?loc id))
+
 let cases_pattern_expr_of_name { CAst.loc; v = na } = CAst.make ?loc @@ match na with
   | Anonymous -> CPatAtom None
   | Name id   -> CPatAtom (Some (qualid_of_ident ?loc id))
@@ -398,6 +404,11 @@ let push_constr subst v = { subst with constrs = v :: subst.constrs }
 let push_item : type s r. s target -> (s, r) entry -> s env -> r -> s env = fun forpat e subst v ->
 match e with
 | TTConstr _ -> push_constr subst v
+| TTIdent ->
+  begin match forpat with
+  | ForConstr -> { subst with binders = (cases_pattern_expr_of_id v, Glob_term.Explicit) :: subst.binders }
+  | ForPattern -> push_constr subst (cases_pattern_expr_of_id v)
+  end
 | TTName ->
   begin match forpat with
   | ForConstr -> { subst with binders = (cases_pattern_expr_of_name v, Glob_term.Explicit) :: subst.binders }
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 116cfc6413..5c329f60a9 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -531,6 +531,10 @@ let warn_deprecated_include_type =
   CWarnings.create ~name:"deprecated-include-type" ~category:"deprecated"
          (fun () -> strbrk "Include Type is deprecated; use Include instead")
 
+let warn_deprecated_as_ident_kind =
+  CWarnings.create ~name:"deprecated-as-ident-kind" ~category:"deprecated"
+         (fun () -> strbrk "grammar kind \"as ident\" no longer accepts \"_\"; use \"as name\" instead to accept \"_\", too, or silence the warning if you actually intended to accept only identifiers.")
+
 }
 
 (* Modules and Sections *)
@@ -1242,7 +1246,13 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
   explicit_subentry:
-    [ [ IDENT "ident" -> { ETIdent } | IDENT "global" -> { ETGlobal }
+    [ [ (* Warning to be turn into an error at the end of deprecation phase (for 8.14) *)
+        IDENT "ident" -> { ETName false }
+        (* To be activated at the end of transitory phase (for 8.15)
+      | IDENT "ident" -> { ETIdent }
+        *)
+      | IDENT "name" -> { ETName true } (* Boolean to remove at the end of transitory phase *)
+      | IDENT "global" -> { ETGlobal }
       | IDENT "bigint" -> { ETBigint }
       | IDENT "binder" -> { ETBinder true }
       | IDENT "constr" -> { ETConstr (InConstrEntry,None,DefaultLevel) }
@@ -1261,8 +1271,9 @@ GRAMMAR EXTEND Gram
       | -> { DefaultLevel } ] ]
   ;
   binder_interp:
-    [ [ "as"; IDENT "ident" -> { Notation_term.AsIdent }
-      | "as"; IDENT "pattern" -> { Notation_term.AsIdentOrPattern }
+    [ [ "as"; IDENT "ident" -> { warn_deprecated_as_ident_kind (); Notation_term.AsIdent }
+      | "as"; IDENT "name" -> { Notation_term.AsName }
+      | "as"; IDENT "pattern" -> { Notation_term.AsNameOrPattern }
       | "as"; IDENT "strict"; IDENT "pattern" -> { Notation_term.AsStrictPattern } ] ]
   ;
 END
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 8759798331..06eb330958 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -340,11 +340,11 @@ let unparsing_metavar i from typs =
   let x = List.nth typs (i-1) in
   let prec,side = unparsing_precedence_of_entry_type from x in
   match x with
-  | ETConstr _ | ETGlobal | ETBigint ->
+  | ETConstr _ | ETGlobal | ETBigint | ETIdent ->
      UnpMetaVar (prec,side)
-  | ETPattern _ | ETIdent ->
+  | ETPattern _ | ETName _ ->
      UnpBinderMetaVar (prec,NotQuotedPattern)
-  | ETBinder _ ->
+  | ETBinder isopen ->
      UnpBinderMetaVar (prec,QuotedPattern)
 
 (* Heuristics for building default printing rules *)
@@ -631,7 +631,8 @@ let include_possible_similar_trailing_pattern typ etyps sl l =
   try_aux 0 l
 
 let prod_entry_type = function
-  | ETIdent -> ETProdName
+  | ETIdent -> ETProdIdent
+  | ETName _ -> ETProdName
   | ETGlobal -> ETProdReference
   | ETBigint -> ETProdBigint
   | ETBinder o -> ETProdOneBinder o
@@ -891,6 +892,11 @@ let default = {
 
 end
 
+(* To be turned into a fatal warning in 8.14 *)
+let warn_deprecated_ident_entry =
+  CWarnings.create ~name:"deprecated-ident-entry" ~category:"deprecated"
+         (fun () -> strbrk "grammar entry \"ident\" permitted \"_\" in addition to proper identifiers; this use is deprecated and its meaning will change in the future; use \"name\" instead.")
+
 let interp_modifiers modl = let open NotationMods in
   let rec interp subtyps acc = function
     | [] -> subtyps, acc
@@ -952,6 +958,13 @@ let interp_modifiers modl = let open NotationMods in
   let subtyps,mods = interp [] default modl in
   (* interpret item levels wrt to main entry *)
   let extra_etyps = List.map (fun (id,bko,n) -> (id,ETConstr (mods.custom,bko,n))) subtyps in
+  (* Temporary hack: "ETName false" (i.e. "ident" in deprecation phase) means "ETIdent" for custom entries *)
+  let mods =
+    { mods with etyps = List.map (function
+        | (id,ETName false) ->
+           if mods.custom = InConstrEntry then (warn_deprecated_ident_entry (); (id,ETName true))
+           else (id,ETIdent)
+        | x -> x) mods.etyps } in
   { mods with etyps = extra_etyps@mods.etyps }
 
 let check_infix_modifiers modifiers =
@@ -1000,7 +1013,7 @@ let set_entry_type from n etyps (x,typ) =
       | ETConstr (s,bko,n), InternalProd ->
           ETConstr (s,bko,(n,InternalProd))
       | ETPattern (b,n), _ -> ETPattern (b,n)
-      | (ETIdent | ETBigint | ETGlobal | ETBinder _ as x), _ -> x
+      | (ETIdent | ETName _ | ETBigint | ETGlobal | ETBinder _ as x), _ -> x
     with Not_found ->
       ETConstr (from,None,(make_lev n from,typ))
   in (x,typ)
@@ -1023,7 +1036,7 @@ let join_auxiliary_recursive_types recvars etyps =
 let internalization_type_of_entry_type = function
   | ETBinder _ -> NtnInternTypeOnlyBinder
   | ETConstr _ | ETBigint | ETGlobal
-  | ETIdent | ETPattern _ -> NtnInternTypeAny
+  | ETIdent | ETName _ | ETPattern _ -> NtnInternTypeAny
 
 let set_internalization_type typs =
   List.map (fun (_, e) -> internalization_type_of_entry_type e) typs
@@ -1043,6 +1056,7 @@ let make_interpretation_type isrec isonlybinding default_if_binding = function
   | ETConstr (_,None,_) -> NtnTypeConstr
   (* Others *)
   | ETIdent -> NtnTypeBinder NtnParsedAsIdent
+  | ETName _ -> NtnTypeBinder NtnParsedAsName
   | ETPattern (ppstrict,_) -> NtnTypeBinder (NtnParsedAsPattern ppstrict) (* Parsed as ident/pattern, primarily interpreted as binder; maybe strict at printing *)
   | ETBigint | ETGlobal -> NtnTypeConstr
   | ETBinder _ ->
@@ -1063,7 +1077,7 @@ let subentry_of_constr_prod_entry from_level = function
   | _ -> InConstrEntrySomeLevel
 
 let make_interpretation_vars
-  (* For binders, default is to parse only as an ident *) ?(default_if_binding=AsIdent)
+  (* For binders, default is to parse only as an ident *) ?(default_if_binding=AsName)
    recvars level allvars typs =
   let eq_subscope (sc1, l1) (sc2, l2) =
     Option.equal String.equal sc1 sc2 &&
@@ -1159,7 +1173,7 @@ let find_precedence custom lev etyps symbols onlyprint =
           user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") in
       (try match List.assoc x etyps, custom with
         | ETConstr (s,_,(NumLevel _ | NextLevel)), s' when s = s' -> test ()
-        | (ETIdent | ETBigint | ETGlobal), _ ->
+        | (ETIdent | ETName _ | ETBigint | ETGlobal), _ ->
             begin match lev with
             | None ->
               ([fun () -> Flags.if_verbose (Feedback.msg_info ?loc:None) (strbrk "Setting notation at level 0.")],0)
@@ -1798,7 +1812,7 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing
       interp_notation_constr env nenv c
   in
   let in_pat id = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,InternalProd))) in
-  let interp = make_interpretation_vars ~default_if_binding:AsIdentOrPattern [] 0 acvars (List.map in_pat vars) in
+  let interp = make_interpretation_vars ~default_if_binding:AsNameOrPattern [] 0 acvars (List.map in_pat vars) in
   let vars = List.map (fun x -> (x, Id.Map.find x interp)) vars in
   let also_in_cases_pattern = has_no_binders_type vars in
   let onlyparsing = onlyparsing || fst (printability None [] false reversibility pat) in
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 4cee4f7a47..01873918aa 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -187,13 +187,16 @@ let level_of_pattern_level = function None -> DefaultLevel | Some n -> NumLevel
 
 let pr_constr_as_binder_kind = let open Notation_term in function
     | AsIdent -> spc () ++ keyword "as ident"
-    | AsIdentOrPattern -> spc () ++ keyword "as pattern"
+    | AsName -> spc () ++ keyword "as name"
+    | AsNameOrPattern -> spc () ++ keyword "as pattern"
     | AsStrictPattern -> spc () ++ keyword "as strict pattern"
 
 let pr_strict b = if b then str "strict " else mt ()
 
 let pr_set_entry_type pr = function
   | ETIdent -> str"ident"
+  | ETName false -> str"ident" (* temporary *)
+  | ETName true -> str"name"
   | ETGlobal -> str"global"
   | ETPattern (b,n) -> pr_strict b ++ str"pattern" ++ pr_at_level (level_of_pattern_level n)
   | ETConstr (s,bko,lev) -> pr_notation_entry s ++ pr lev ++ pr_opt pr_constr_as_binder_kind bko
@@ -268,9 +271,9 @@ let pr_reference_or_constr pr_c = function
   | HintsConstr c -> pr_c c
 
 let pr_hint_mode = let open Hints in function
-    | ModeInput -> str"+"
-    | ModeNoHeadEvar -> str"!"
-    | ModeOutput -> str"-"
+  | ModeInput -> str"+"
+  | ModeNoHeadEvar -> str"!"
+  | ModeOutput -> str"-"
 
 let pr_hint_info pr_pat { Typeclasses.hint_priority = pri; hint_pattern = pat } =
   pr_opt (fun x -> str"|" ++ int x) pri ++