Making Hints generic in the use of external tactics.

2 files changed, 6 insertions, 10 deletions

diff --git a/tactics/hints.ml b/tactics/hints.ml
index 9ee9e798b..a6d1fc6c8 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -804,7 +804,6 @@ let make_unfold eref =
      code = with_uid (Unfold_nth eref) })
 
 let make_extern pri pat tacast =
-  let tacast = Genarg.in_gen (Genarg.glbwit Constrarg.wit_ltac) tacast in
   let hdconstr = Option.map try_head_pattern pat in
   (hdconstr,
    { pri = pri;
@@ -1082,8 +1081,6 @@ let add_trivials env sigma l local dbnames =
       Lib.add_anonymous_leaf (inAutoHint hint))
     dbnames
 
-let (forward_intern_tac, extern_intern_tac) = Hook.make ()
-
 type hnf = bool
 
 type hints_entry =
@@ -1094,7 +1091,7 @@ type hints_entry =
   | HintsTransparencyEntry of evaluable_global_reference list * bool
   | HintsModeEntry of global_reference * hint_mode list
   | HintsExternEntry of
-      int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr
+      int * (patvar list * constr_pattern) option * Genarg.glob_generic_argument
 
 let default_prepare_hint_ident = Id.of_string "H"
 
@@ -1184,7 +1181,9 @@ let interp_hints poly =
   | HintsExtern (pri, patcom, tacexp) ->
       let pat =	Option.map fp patcom in
       let l = match pat with None -> [] | Some (l, _) -> l in
-      let tacexp = Hook.get forward_intern_tac l tacexp in
+      let ltacvars = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in
+      let env = Genintern.({ genv = env; ltacvars }) in
+      let _, tacexp = Genintern.generic_intern env tacexp in
       HintsExternEntry (pri, pat, tacexp)
 
 let add_hints local dbnames0 h =
diff --git a/tactics/hints.mli b/tactics/hints.mli
index e38daca92..83876be84 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -134,7 +134,7 @@ type hints_entry =
   | HintsTransparencyEntry of evaluable_global_reference list * bool
   | HintsModeEntry of global_reference * hint_mode list
   | HintsExternEntry of
-      int * (patvar list * constr_pattern) option * Tacexpr.glob_tactic_expr
+      int * (patvar list * constr_pattern) option * Genarg.glob_generic_argument
 
 val searchtable_map : hint_db_name -> hint_db
 
@@ -201,7 +201,7 @@ val make_resolve_hyp :
 (** [make_extern pri pattern tactic_expr] *)
 
 val make_extern :
-  int -> constr_pattern option -> Tacexpr.glob_tactic_expr
+  int -> constr_pattern option -> Genarg.glob_generic_argument
       -> hint_entry
 
 val run_hint : hint ->
@@ -211,9 +211,6 @@ val run_hint : hint ->
     written code. *)
 val repr_hint : hint -> (raw_hint * clausenv) hint_ast
 
-val extern_intern_tac :
-  (patvar list -> Genarg.raw_generic_argument -> Tacexpr.glob_tactic_expr) Hook.t
-
 (** Create a Hint database from the pairs (name, constr).
    Useful to take the current goal hypotheses as hints;
    Boolean tells if lemmas with evars are allowed *)