Renaming "ident" into "name" in grammar entries, to prevent confusions.

We use a deprecation phase where:
- "ident" means "name" (as it used to mean), except in custom coercion
  entries where it already meant "ident".
- "ident" will be made again available (outside situation of
  coercions) to mean "ident" at the end of deprecation phase.

Also renaming "as ident" into "as name".

Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>

11 files changed, 87 insertions, 20 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/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/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..00a5727af6 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