Useless hooks in Tacintern.

4 files changed, 3 insertions, 16 deletions

diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 7a1e34ca2..4c8175b8d 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -65,10 +65,6 @@ let interp_ml_tactic s =
     Errors.errorlabstrm ""
       (str "The tactic " ++ str (pr_tacname s) ++ str " is not installed.")
 
-let () =
-  let assert_installed opn = let _ = interp_ml_tactic opn in () in
-  Hook.set Tacintern.assert_tactic_installed_hook assert_installed
-
 (***************************************************************************)
 (* Tactic registration *)
 
@@ -121,6 +117,3 @@ let register_ltac local id tac =
 
 let redefine_ltac local kn tac =
   Lib.add_anonymous_leaf (inMD (local, Some kn, tac))
-
-let () =
-  Hook.set Tacintern.interp_ltac_hook interp_ltac
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 4ffaa2b0a..6f6f144c1 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -134,8 +134,6 @@ let intern_move_location ist = function
   | MoveFirst -> MoveFirst
   | MoveLast -> MoveLast
 
-let (f_interp_ltac, interp_ltac_hook) = Hook.make ()
-
 (* Internalize an isolated reference in position of tactic *)
 
 let intern_isolated_global_tactic_reference r =
@@ -444,8 +442,6 @@ let clause_app f = function
   | { onhyps=Some l; concl_occs=nl } ->
       { onhyps=Some(List.map f l); concl_occs=nl}
 
-let (f_assert_tactic_installed, assert_tactic_installed_hook) = Hook.make ()
-
 let map_raw wit f ist x =
   in_gen (glbwit wit) (f ist (out_gen (rawwit wit) x))
 
@@ -632,7 +628,7 @@ and intern_tactic_seq onlytac ist = function
       let l = List.map (fun (id,a) -> (id,intern_genarg ist a)) l in
       ist.ltacvars, TacAlias (loc,s,l)
   | TacML (loc,opn,l) ->
-      let () = Hook.get f_assert_tactic_installed opn in
+      let () = ignore (Tacenv.interp_ml_tactic opn) in
       ist.ltacvars, TacML (adjust_loc loc,opn,List.map (intern_genarg ist) l)
 
 and intern_tactic_as_arg loc onlytac ist a =
@@ -777,7 +773,7 @@ let pr_ltac_fun_arg = function
 let print_ltac id =
  try
   let kn = Nametab.locate_tactic id in
-  let l,t = split_ltac_fun (Hook.get f_interp_ltac kn) in
+  let l,t = split_ltac_fun (Tacenv.interp_ltac kn) in
   hv 2 (
     hov 2 (str "Ltac" ++ spc() ++ pr_qualid id ++
            prlist pr_ltac_fun_arg l ++ spc () ++ str ":=")
diff --git a/tactics/tacintern.mli b/tactics/tacintern.mli
index 2f6eb60f4..9ca2477cf 100644
--- a/tactics/tacintern.mli
+++ b/tactics/tacintern.mli
@@ -63,6 +63,4 @@ val intern_red_expr : glob_sign -> raw_red_expr -> glob_red_expr
 val dump_glob_red_expr : raw_red_expr -> unit
 
 (* Hooks *)
-val assert_tactic_installed_hook : (ml_tactic_name -> unit) Hook.t
-val interp_ltac_hook : (KerName.t -> glob_tactic_expr) Hook.t
 val strict_check : bool ref
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 4eb4318ee..d2f02d77f 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -16,8 +16,8 @@ Inv
 Leminv
 Tacsubst
 Taccoerce
-Tacintern
 Tacenv
+Tacintern
 TacticMatching
 Tacinterp
 Evar_tactics