Use a new namespace for Hint Extern names

plugins/ltac/g_ltac.mlg

@@ -64,6 +64,12 @@ let toplevel_selector = G_vernac.toplevel_selector
 let subprf = G_vernac.subprf
 let subprf_with_selector = G_vernac.subprf_with_selector
 
+let lname_of_lident : lident -> lname =
+  CAst.map (fun s -> Name s)
+
+let name_of_ident_decl : ident_decl -> name_decl =
+  on_fst lname_of_lident
+
 }
 
 GRAMMAR EXTEND Gram
@@ -295,7 +301,7 @@ GRAMMAR EXTEND Gram
   ;
   hint: TOP
     [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern;
-        name = OPT [ "as"; q = qualid -> { q } ];
+        name = OPT [ "as"; id = ident_decl -> { name_of_ident_decl id } ];
         "=>"; tac = Pltac.tactic ->
           { Vernacexpr.HintsExtern (n,c, in_tac tac, name) } ] ]
   ;

vernac/comHints.ml

@@ -88,6 +88,45 @@ let rectify_hint_constr h = match h with
   | CAppExpl ((qid, None), []) -> Vernacexpr.HintsReference qid
   | _ -> Vernacexpr.HintsConstr c
 
+(* Hint Extern names *)
+
+open Libnames
+
+module FullPath =
+struct
+  type t = full_path
+  let equal = eq_full_path
+  let to_string = string_of_path
+  let repr sp =
+    let dir,id = repr_path sp in
+    id, (DirPath.repr dir)
+end
+
+module KnTab = Nametab.Make(FullPath)(KerName)
+
+type nametab = {
+  tab_cstr : KnTab.t;
+  tab_cstr_rev : full_path KNmap.t;  (* needed? *)
+}
+
+let empty_nametab = {
+  tab_cstr = KnTab.empty;
+  tab_cstr_rev = KNmap.empty;
+}
+
+let nametab = Summary.ref empty_nametab ~name:"hintextern-nametab"
+
+(* todo: pick better names *)
+let push_constructor vis sp kn =
+  let tab = !nametab in
+  let tab_cstr = KnTab.push vis sp kn tab.tab_cstr in
+  let tab_cstr_rev = KNmap.add kn sp tab.tab_cstr_rev in
+  nametab := { tab_cstr; tab_cstr_rev }
+
+let locate_constructor qid =
+  let tab = !nametab in
+  KnTab.locate qid tab.tab_cstr
+
 let interp_hints ~poly h =
   let env = Global.env () in
   let sigma = Evd.from_env env in
@@ -166,5 +205,6 @@ let interp_hints ~poly h =
     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
+    (* todo: call push_constructor here *)
     HintsExternEntry
       ({Typeclasses.hint_priority = Some pri; hint_pattern = pat}, tacexp, globref)

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 * Libnames.qualid option
+  | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument * Constrexpr.name_decl option
 
 (** [synterp_vernac_expr] describes the AST of commands which have effects on
     parsing or parsing extensions *)