Let users specify a hint name on Hint Extern

doc/changelog/08-vernac-commands-and-options/19824-hint_extern_name.rst

@@ -0,0 +1,6 @@
+- **Added:**
+  Provide a way to associate a name with a :cmd:`Hint Extern` so that :cmd:`Remove Hints`
+  and :cmd:`Hint Cut` can refer to them
+  (`#19824 <https://github.com/coq/coq/pull/19824>`_,
+  fixes `#19816 <https://github.com/coq/coq/issues/19816>`_,
+  by Jim Fehrle).

doc/sphinx/proofs/automatic-tactics/auto.rst

@@ -513,11 +513,12 @@ Creating Hints
       These flags affect the unification of hints in the database.
       We advise using this just after a :cmd:`Create HintDb` command.
 
-   .. cmd:: Hint Extern @natural {? @one_pattern } => @ltac_expr {? : {+ @ident } }
+   .. cmd:: Hint Extern @natural {? @one_pattern } {? as @qualid } => @ltac_expr {? : {+ @ident } }
 
       Extends :tacn:`auto` with tactics other than :tacn:`apply` and
       :tacn:`unfold`. :n:`@natural` is the cost, :n:`@one_pattern` is the pattern
-      to match and :n:`@ltac_expr` is the action to apply.
+      to match, :n:`@qualid` is an existing name to associate with the hint (e.g.
+      for use in :cmd:`Remove Hints`) and :n:`@ltac_expr` is the action to apply.
 
       **Usage tip**: tactics that can succeed even if they don't change the context,
       such as most of the :ref:`conversion tactics <applyingconversionrules>`, should
@@ -723,6 +724,8 @@ Creating Hints
    the symbol name.  Note that hints with the same cost are tried in
    reverse of the order they're defined in, i.e., last to first.
 
+   .. todo describe name for Extern
+
 Hint locality
 `````````````
 

doc/tools/docgram/common.edit_mlg

@@ -33,8 +33,8 @@ hint: [
 | WITH [ "Transparent" | "Opaque" ] LIST1 global
 | DELETE "Opaque" LIST1 global
 
-| REPLACE "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic
-| WITH "Extern" natural OPT constr_pattern "=>" tactic
+| REPLACE "Extern" natural OPT Constr.constr_pattern OPT [ "as" qualid ] "=>" Pltac.tactic
+| WITH "Extern" natural OPT constr_pattern OPT [ "as" qualid ] "=>" tactic
 | INSERTALL "Hint"
 | APPENDALL opt_hintbases
 ]

doc/tools/docgram/fullGrammar

@@ -729,7 +729,7 @@ hint: [
 | "Mode" global mode
 | "Unfold" LIST1 global
 | "Constructors" LIST1 global
-| "Extern" natural OPT Constr.constr_pattern "=>" Pltac.tactic
+| "Extern" natural OPT Constr.constr_pattern OPT [ "as" qualid ] "=>" Pltac.tactic
 ]
 
 constr_body: [

doc/tools/docgram/orderedGrammar

@@ -1004,7 +1004,7 @@ command: [
 | "Hint" "Mode" qualid LIST1 [ "+" | "!" | "-" ] OPT ( ":" LIST1 ident )
 | "Hint" "Unfold" LIST1 qualid OPT ( ":" LIST1 ident )
 | "Hint" "Constructors" LIST1 qualid OPT ( ":" LIST1 ident )
-| "Hint" "Extern" natural OPT one_pattern "=>" ltac_expr OPT ( ":" LIST1 ident )
+| "Hint" "Extern" natural OPT one_pattern OPT [ "as" qualid ] "=>" ltac_expr OPT ( ":" LIST1 ident )
 | "Time" sentence
 | "Instructions" sentence
 | "Profile" OPT string sentence

plugins/ltac/g_ltac.mlg

@@ -294,9 +294,10 @@ GRAMMAR EXTEND Gram
           { Vernacexpr.VernacSynPure (Vernacexpr.VernacProof (Some (in_tac ta),Some l)) } ] ]
   ;
   hint: TOP
-    [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>";
-        tac = Pltac.tactic ->
-        { Vernacexpr.HintsExtern (n,c, in_tac tac) } ] ]
+    [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern;
+        name = OPT [ "as"; q = qualid -> { q } ];
+        "=>"; tac = Pltac.tactic ->
+          { Vernacexpr.HintsExtern (n,c, in_tac tac, name) } ] ]
   ;
   term: LEVEL "0"
     [ [ IDENT "ltac"; ":"; "("; tac = Pltac.ltac_expr; ")" ->

tactics/hints.ml

@@ -988,7 +988,7 @@ let make_unfold eref =
      secvars = secvars_of_global (Global.env ()) g;
      code = with_uid (Unfold_nth eref) })
 
-let make_extern pri pat tacast =
+let make_extern pri pat tacast name =
   let hdconstr = match pat with
   | None -> None
   | Some c ->
@@ -1000,7 +1000,7 @@ let make_extern pri pat tacast =
   (hdconstr,
    { pri = pri;
      pat = Option.map (fun p -> SyntacticPattern p) pat;
-     name = None;
+     name = name;
      db = ();
      secvars = Id.Pred.empty; (* Approximation *)
      code = with_uid (Extern (pat, tacast)) })
@@ -1434,17 +1434,17 @@ let add_transparency l b ~locality dbnames =
       Lib.add_leaf (inAutoHint hint))
     dbnames
 
-let add_extern info tacast ~locality dbname =
+let add_extern info tacast name ~locality dbname =
   let pat = match info.hint_pattern with
   | None -> None
   | Some (_, pat) -> Some pat
   in
   let hint = make_hint ~locality dbname
-                       (AddHints [make_extern (Option.get info.hint_priority) pat tacast]) in
+       (AddHints [make_extern (Option.get info.hint_priority) pat tacast name]) in
   Lib.add_leaf (inAutoHint hint)
 
-let add_externs info tacast ~locality dbnames =
-  List.iter (add_extern info tacast ~locality) dbnames
+let add_externs info tacast name ~locality dbnames =
+  List.iter (add_extern info tacast name ~locality) dbnames
 
 let add_trivials env sigma l ~locality dbnames =
   List.iter
@@ -1465,7 +1465,7 @@ type hints_entry =
   | HintsUnfoldEntry of Evaluable.t list
   | HintsTransparencyEntry of Evaluable.t hints_transparency_target * bool
   | HintsModeEntry of GlobRef.t * hint_mode list
-  | HintsExternEntry of hint_info * Genarg.glob_generic_argument
+  | HintsExternEntry of hint_info * Genarg.glob_generic_argument * GlobRef.t option
 
 let default_prepare_hint_ident = Id.of_string "H"
 
@@ -1540,8 +1540,8 @@ let add_hints ~locality dbnames h =
   | HintsUnfoldEntry lhints -> add_unfolds lhints ~locality dbnames
   | HintsTransparencyEntry (lhints, b) ->
       add_transparency lhints b ~locality dbnames
-  | HintsExternEntry (info, tacexp) ->
-      add_externs info tacexp ~locality dbnames
+  | HintsExternEntry (info, tacexp, name) ->
+      add_externs info tacexp name ~locality dbnames
 
 let hint_globref gr = IsGlobRef gr
 
@@ -1629,8 +1629,15 @@ let pr_id_hint env sigma (id, v) =
   | Some (ConstrPattern p | SyntacticPattern p) -> str", pattern " ++ pr_lconstr_pattern_env env sigma p
   | Some DefaultPattern -> str", pattern " ++ pr_leconstr_env env sigma (get_default_pattern v.code.obj)
   in
+  let ename =
+    match v.code.obj, v.name with
+    | Extern _, Some n ->
+      let qstr = string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty n) in
+      str ", name " ++ str qstr
+    | _ -> mt ()
+  in
   (pr_hint env sigma v.code ++ str" (cost " ++ int v.pri ++ pr_pat v
-   ++ str", id " ++ int id ++ str ")")
+   ++ str", id " ++ int id ++ ename ++ str ")")
 
 let pr_hint_list env sigma hintlist =
   (str "  " ++ hov 0 (prlist_with_sep fnl (pr_id_hint env sigma) hintlist) ++ fnl ())

tactics/hints.mli

@@ -167,7 +167,7 @@ type hints_entry =
   | HintsUnfoldEntry of Evaluable.t list
   | HintsTransparencyEntry of Evaluable.t hints_transparency_target * bool
   | HintsModeEntry of GlobRef.t * hint_mode list
-  | HintsExternEntry of hint_info * Genarg.glob_generic_argument
+  | HintsExternEntry of hint_info * Genarg.glob_generic_argument * GlobRef.t option
 
 val searchtable_map : hint_db_name -> hint_db
 

test-suite/output/extern_name.out

@@ -0,0 +1,16 @@
+Non-discriminated database
+Unfoldable variable definitions: none
+Unfoldable constant definitions: none
+Unfoldable projection definitions: none
+Cut: emp
+For any goal ->   
+For True ->   (*external*) idtac "x" (cost 1, pattern True, id 0, name Nat.t)
+
+Non-discriminated database
+Unfoldable variable definitions: none
+Unfoldable constant definitions: none
+Unfoldable projection definitions: none
+Cut: emp
+For any goal ->   
+For True ->   
+

test-suite/output/extern_name.v

@@ -0,0 +1,4 @@
+Hint Extern 1 True as Stdlib.Init.Nat.t => idtac "x" : db.
+Print HintDb db.
+Remove Hints Init.Nat.t : db.
+Print HintDb db.

vernac/comHints.ml

@@ -160,10 +160,11 @@ let interp_hints ~poly h =
           , hint_globref gr ))
     in
     HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
-  | HintsExtern (pri, patcom, tacexp) ->
+  | HintsExtern (pri, patcom, tacexp, name) ->
     let pat = Option.map (fp sigma) patcom in
     let ltacvars = match pat with None -> Id.Set.empty | Some (l, _) -> l in
     let env = Genintern.{(empty_glob_sign ~strict:true env) with ltacvars} in
     let _, tacexp = Genintern.generic_intern env tacexp in
+    let globref = Option.cata (fun n -> Some (Nametab.global n)) None name in
     HintsExternEntry
-      ({Typeclasses.hint_priority = Some pri; hint_pattern = pat}, tacexp)
+      ({Typeclasses.hint_priority = Some pri; hint_pattern = pat}, tacexp, globref)

vernac/ppvernac.ml

@@ -339,9 +339,13 @@ let pr_hints db h pr_c pr_pat =
     | HintsConstructors c ->
       keyword "Constructors"
       ++ spc() ++ prlist_with_sep spc pr_qualid c
-    | HintsExtern (n,c,tac) ->
+    | HintsExtern (n,c,tac,name) ->
       let pat = match c with None -> mt () | Some pat -> pr_pat pat in
-      keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ str" =>" ++
+      let nstr = match name with
+        | Some n -> str " as " ++ str (Libnames.string_of_qualid n)
+        | None -> mt ()
+      in
+      keyword "Extern" ++ spc() ++ int n ++ spc() ++ pat ++ nstr ++ str" =>" ++
       spc() ++ pr_gen tac
   in
   hov 2 (keyword "Hint "++ pph ++ opth)

vernac/vernacexpr.mli

@@ -371,7 +371,7 @@ type hints_expr =
   | HintsTransparency of Libnames.qualid Hints.hints_transparency_target * bool
   | HintsMode of Libnames.qualid * Hints.hint_mode list
   | HintsConstructors of Libnames.qualid list
-  | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument
+  | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument * Libnames.qualid option
 
 (** [synterp_vernac_expr] describes the AST of commands which have effects on
     parsing or parsing extensions *)