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>

4 files changed, 52 insertions, 13 deletions

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