Use the Hook module here and there.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16510 85f007b7-540e-0410-9357-904b9bb8a0f7

36 files changed, 137 insertions, 215 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 4f88a6b0e..d664ebd0c 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -34,19 +34,12 @@ type internal_flag =
 
 (** XML output hooks *)
 
-let xml_declare_variable = ref (fun (sp:object_name) -> ())
-let xml_declare_constant = ref (fun (sp:internal_flag * constant)-> ())
-let xml_declare_inductive = ref (fun (sp:internal_flag * object_name) -> ())
+let (f_xml_declare_variable, xml_declare_variable) = Hook.make ~default:ignore ()
+let (f_xml_declare_constant, xml_declare_constant) = Hook.make ~default:ignore ()
+let (f_xml_declare_inductive, xml_declare_inductive) = Hook.make ~default:ignore ()
 
 let if_xml f x = if !Flags.xml_export then f x else ()
 
-let set_xml_declare_variable f = xml_declare_variable := if_xml f
-let set_xml_declare_constant f = xml_declare_constant := if_xml f
-let set_xml_declare_inductive f = xml_declare_inductive := if_xml f
-
-let cache_hook = ref ignore
-let add_cache_hook f = cache_hook := f
-
 (** Declaration of section variables and local definitions *)
 
 type section_variable_entry =
@@ -94,7 +87,7 @@ let declare_variable id obj =
   declare_var_implicits id;
   Notation.declare_ref_arguments_scope (VarRef id);
   Heads.declare_head (EvalVarRef id);
-  !xml_declare_variable oname;
+  if_xml (Hook.get f_xml_declare_variable) oname;
   oname
 
 
@@ -142,8 +135,7 @@ let cache_constant ((sp,kn), obj) =
   Nametab.push (Nametab.Until 1) sp (ConstRef (constant_of_kn kn));
   add_section_constant kn' (Global.lookup_constant kn').const_hyps;
   Dischargedhypsmap.set_discharged_hyps sp obj.cst_hyps;
-  add_constant_kind (constant_of_kn kn) obj.cst_kind;
-  !cache_hook sp
+  add_constant_kind (constant_of_kn kn) obj.cst_kind
 
 let discharged_hyps kn sechyps =
   let (_,dir,_) = repr_kn kn in
@@ -197,7 +189,7 @@ let declare_constant ?(internal = UserVerbose) ?(local = false) id (cd, kind) =
     cst_locl = local;
   } in
   let kn = declare_constant_common id cst in
-  let () = !xml_declare_constant (internal, kn) in
+  let () = if_xml (Hook.get f_xml_declare_constant) (internal, kn) in
   kn
 
 let declare_definition ?(internal=UserVerbose)
@@ -260,9 +252,7 @@ let cache_inductive ((sp,kn),(dhyps,mie)) =
   assert (eq_mind kn' (mind_of_kn kn));
   add_section_kn kn' (Global.lookup_mind kn').mind_hyps;
   Dischargedhypsmap.set_discharged_hyps sp dhyps;
-  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names;
-  List.iter (fun (sp,_) -> !cache_hook sp) (inductive_names sp kn mie)
-
+  List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
 
 let discharge_inductive ((sp,kn),(dhyps,mie)) =
   let mind = Global.mind_of_delta_kn kn in
@@ -306,7 +296,7 @@ let declare_mind isrecord mie =
   let mind = Global.mind_of_delta_kn kn in
   declare_mib_implicits mind;
   declare_inductive_argument_scopes mind mie;
-  !xml_declare_inductive (isrecord,oname);
+  if_xml (Hook.get f_xml_declare_inductive) (isrecord,oname);
   oname
 
 (* Declaration messages *)
diff --git a/library/declare.mli b/library/declare.mli
index a9cd8f720..ff4e20ad2 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -67,12 +67,9 @@ val declare_definition :
 val declare_mind : internal_flag -> mutual_inductive_entry -> object_name
 
 (** Hooks for XML output *)
-val set_xml_declare_variable : (object_name -> unit) -> unit
-val set_xml_declare_constant : (internal_flag * constant -> unit) -> unit
-val set_xml_declare_inductive : (internal_flag * object_name -> unit) -> unit
-
-(** Hook for the cache function of constants and inductives *)
-val add_cache_hook : (full_path -> unit) -> unit
+val xml_declare_variable : (object_name -> unit) Hook.t
+val xml_declare_constant : (internal_flag * constant -> unit) Hook.t
+val xml_declare_inductive : (internal_flag * object_name -> unit) Hook.t
 
 (** Declaration messages *)
 
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 894445de1..15a964792 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -600,11 +600,7 @@ let start_library dir =
   Lib.start_compilation dir mp;
   Lib.add_frozen_state ()
 
-let end_library_hook = ref ignore
-let set_end_library_hook f = end_library_hook := f
-
 let end_library dir =
-  !end_library_hook();
   let prefix, lib_stack = Lib.end_compilation dir in
   let mp,cenv,ast = Global.export dir in
   let substitute, keep, _ = Lib.classify_segment lib_stack in
diff --git a/library/declaremods.mli b/library/declaremods.mli
index c5a43dfbf..06a4edd84 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -95,9 +95,6 @@ val end_library :
   library_name ->
     Safe_typing.compiled_library * library_objects * Safe_typing.native_library
 
-(** set a function to be executed at end_library *)
-val set_end_library_hook : (unit -> unit) -> unit
-
 (** [really_import_module mp] opens the module [mp] (in a Caml sense).
    It modifies Nametab and performs the [open_object] function for
    every object of the module. Raises [Not_found] when [mp] is unknown. *)
diff --git a/library/lib.ml b/library/lib.ml
index 0ba9fd919..bf4c0a474 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -475,11 +475,8 @@ let is_in_section ref =
 (* Sections. *)
 
 (* XML output hooks *)
-let xml_open_section = ref (fun id -> ())
-let xml_close_section = ref (fun id -> ())
-
-let set_xml_open_section f = xml_open_section := f
-let set_xml_close_section f = xml_close_section := f
+let (f_xml_open_section, xml_open_section) = Hook.make ~default:ignore ()
+let (f_xml_close_section, xml_close_section) = Hook.make ~default:ignore ()
 
 let open_section id =
   let olddir,(mp,oldsec) = !path_prefix in
@@ -493,7 +490,7 @@ let open_section id =
   (*Pushed for the lifetime of the section: removed by unfrozing the summary*)
   Nametab.push_dir (Nametab.Until 1) dir (DirOpenSection prefix);
   path_prefix := prefix;
-  if !Flags.xml_export then !xml_open_section id;
+  if !Flags.xml_export then Hook.get f_xml_open_section id;
   add_section ()
 
 
@@ -522,7 +519,7 @@ let close_section () =
   let full_olddir = fst !path_prefix in
   pop_path_prefix ();
   add_entry oname (ClosedSection (List.rev (mark::secdecls)));
-  if !Flags.xml_export then !xml_close_section (basename (fst oname));
+  if !Flags.xml_export then Hook.get f_xml_close_section (basename (fst oname));
   let newdecls = List.map discharge_item secdecls in
   Summary.unfreeze_summaries fs;
   List.iter (Option.iter (fun (id,o) -> add_discharged_leaf id o)) newdecls;
diff --git a/library/lib.mli b/library/lib.mli
index 8ab98f775..c9b2047bc 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -178,8 +178,8 @@ val unfreeze : frozen -> unit
 val init : unit -> unit
 
 (** XML output hooks *)
-val set_xml_open_section : (Names.Id.t -> unit) -> unit
-val set_xml_close_section : (Names.Id.t -> unit) -> unit
+val xml_open_section : (Names.Id.t -> unit) Hook.t
+val xml_close_section : (Names.Id.t -> unit) Hook.t
 
 (** {6 Section management for discharge } *)
 type variable_info = Names.Id.t * Decl_kinds.binding_kind *
diff --git a/library/library.ml b/library/library.ml
index 52d3a5d1d..472b1fb1d 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -498,8 +498,7 @@ let in_require : require_obj -> obj =
 (* Require libraries, import them if [export <> None], mark them for export
    if [export = Some true] *)
 
-let xml_require = ref (fun d -> ())
-let set_xml_require f = xml_require := f
+let (f_xml_require, xml_require) = Hook.make ~default:ignore ()
 
 let require_library_from_dirpath modrefl export =
   let needed = List.fold_left rec_intern_library [] modrefl in
@@ -514,7 +513,7 @@ let require_library_from_dirpath modrefl export =
       end
     else
       add_anonymous_leaf (in_require (needed,modrefl,export));
-    if !Flags.xml_export then List.iter !xml_require modrefl;
+    if !Flags.xml_export then List.iter (Hook.get f_xml_require) modrefl;
   add_frozen_state ()
 
 let require_library qidl export =
@@ -531,7 +530,7 @@ let require_library_from_file idopt file export =
   end
   else
     add_anonymous_leaf (in_require (needed,[modref],export));
-  if !Flags.xml_export then !xml_require modref;
+  if !Flags.xml_export then Hook.get f_xml_require modref;
   add_frozen_state ()
 
 (* the function called by Vernacentries.vernac_import *)
diff --git a/library/library.mli b/library/library.mli
index 22b94e521..8ed3afd66 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -56,7 +56,7 @@ val library_full_filename : DirPath.t -> string
 val overwrite_library_filenames : string -> unit
 
 (** {6 Hook for the xml exportation of libraries } *)
-val set_xml_require : (DirPath.t -> unit) -> unit
+val xml_require : (DirPath.t -> unit) Hook.t
 
 (** {6 Locate a library in the load paths } *)
 exception LibUnmappedDir
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index bf30d9d35..81cfd3f1d 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -288,8 +288,7 @@ let rec string in_comments bp len = parser
   | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string
 
 (* Hook for exporting comment into xml theory files *)
-let xml_output_comment = ref (fun _ -> ())
-let set_xml_output_comment f = xml_output_comment := f
+let (f_xml_output_comment, xml_output_comment) = Hook.make ~default:ignore ()
 
 (* Utilities for comments in beautify *)
 let comment_begin = ref None
@@ -335,7 +334,7 @@ let comment_stop ep =
   let current_s = Buffer.contents current in
   if !Flags.xml_export && Buffer.length current > 0 &&
     (!between_com || not(null_comment current_s)) then
-      !xml_output_comment current_s;
+      Hook.get f_xml_output_comment current_s;
   (if Flags.do_beautify() && Buffer.length current > 0 &&
     (!between_com || not(null_comment current_s)) then
     let bp = match !comment_begin with
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index cef53a871..8eef2f63c 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -31,7 +31,7 @@ type com_state
 val com_state: unit -> com_state
 val restore_com_state: com_state -> unit
 
-val set_xml_output_comment : (string -> unit) -> unit
+val xml_output_comment : (string -> unit) Hook.t
 
 val terminal : string -> Tok.t
 
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index a6a9838ae..5c67c33b6 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -110,7 +110,7 @@ let rec type_scheme_nb_args env c =
 	if is_info_scheme env t then n+1 else n
     | _ -> 0
 
-let _ = register_type_scheme_nb_args type_scheme_nb_args
+let _ = Hook.set type_scheme_nb_args_hook type_scheme_nb_args
 
 (*s [type_sign_vl] does the same, plus a type var list. *)
 
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index ebe7230ec..581735736 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -755,8 +755,7 @@ let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ())
 (*s Extract Constant/Inductive. *)
 
 (* UGLY HACK: to be defined in [extraction.ml] *)
-let use_type_scheme_nb_args, register_type_scheme_nb_args =
-  let r = ref (fun _ _ -> 0) in (fun x y -> !r x y), (:=) r
+let (use_type_scheme_nb_args, type_scheme_nb_args_hook) = Hook.make ()
 
 let customs = Summary.ref Refmap'.empty ~name:"ExtrCustom"
 
@@ -823,7 +822,7 @@ let extract_constant_inline inline r ids s =
 	let typ = Reduction.whd_betadeltaiota env typ in
 	if Reduction.is_arity env typ
 	  then begin
-	    let nargs = use_type_scheme_nb_args env typ in
+	    let nargs = Hook.get use_type_scheme_nb_args env typ in
 	    if List.length ids <> nargs then error_axiom_scheme g nargs
 	  end;
 	Lib.add_anonymous_leaf (inline_extraction (inline,[g]));
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 53acccf84..ce6f8e229 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -171,7 +171,7 @@ val implicits_of_global : global_reference -> int list
 (*s Table for user-given custom ML extractions. *)
 
 (* UGLY HACK: registration of a function defined in [extraction.ml] *)
-val register_type_scheme_nb_args : (Environ.env -> Term.constr -> int) -> unit
+val type_scheme_nb_args_hook : (Environ.env -> Term.constr -> int) Hook.t
 
 val is_custom : global_reference -> bool
 val is_inline_custom : global_reference -> bool
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index ddc4725c3..6145548b2 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -441,12 +441,7 @@ let proof_to_export = ref None (* holds the proof-tree to export *)
 ;;
 
 let _ =
-  Pfedit.set_xml_cook_proof
-   (function pftreestate -> proof_to_export := Some pftreestate)
-;;
-
-let _ =
-  Declare.set_xml_declare_variable
+  Hook.set Declare.xml_declare_variable
    (function (sp,kn) ->
      let id = Libnames.basename sp in
      print Declare.UserVerbose (Globnames.VarRef id) (kind_of_variable id) xml_library_root ;
@@ -454,7 +449,7 @@ let _ =
 ;;
 
 let _ =
-  Declare.set_xml_declare_constant
+  Hook.set Declare.xml_declare_constant
    (function (internal,kn) ->
      match !proof_to_export with
         None ->
@@ -470,7 +465,7 @@ let _ =
 ;;
 
 let _ =
-  Declare.set_xml_declare_inductive
+  Hook.set Declare.xml_declare_inductive
    (function (isrecord,(sp,kn)) ->
       print Declare.UserVerbose (Globnames.IndRef (Names.mind_of_kn kn,0))
         (kind_of_inductive isrecord (Names.mind_of_kn kn))
@@ -478,7 +473,7 @@ let _ =
 ;;
 
 let _ =
-  Vernac.set_xml_start_library
+  Hook.set Vernac.xml_start_library
    (function () ->
      Buffer.reset theory_buffer;
      theory_output_string "<?xml version=\"1.0\" encoding=\"latin1\"?>\n";
@@ -495,7 +490,7 @@ let _ =
 ;;
 
 let _ =
-  Vernac.set_xml_end_library
+  Hook.set Vernac.xml_end_library
    (function () ->
       theory_output_string "</body>\n</html>\n";
       let ofn = theory_filename xml_library_root in
@@ -525,7 +520,7 @@ let _ =
        ofn)
 ;;
 
-let _ = Lexer.set_xml_output_comment (theory_output_string ~do_not_quote:true) ;;
+let _ = Hook.set Lexer.xml_output_comment (theory_output_string ~do_not_quote:true) ;;
 
 let uri_of_dirpath dir =
   "/" ^ String.concat "/"
@@ -533,19 +528,19 @@ let uri_of_dirpath dir =
 ;;
 
 let _ =
-  Lib.set_xml_open_section
+  Hook.set Lib.xml_open_section
     (fun _ ->
       let s = "cic:" ^ uri_of_dirpath (Lib.cwd ()) in
       theory_output_string ("<ht:SECTION uri=\""^s^"\">"))
 ;;
 
 let _ =
-  Lib.set_xml_close_section
+  Hook.set Lib.xml_close_section
     (fun _ -> theory_output_string "</ht:SECTION>")
 ;;
 
 let _ =
-  Library.set_xml_require
+  Hook.set Library.xml_require
     (fun d -> theory_output_string
       (Printf.sprintf "<b>Require</b> <a helm:helm_link=\"href\" href=\"theory:%s.theory\">%s</a>.<br/>"
        (uri_of_dirpath d) (Names.DirPath.to_string d)))
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 4dc6280f1..24b084e9b 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -21,24 +21,17 @@ open Libobject
 (*i*)
 
 
-let add_instance_hint_ref = ref (fun id path local pri -> assert false)
-let register_add_instance_hint =
-  (:=) add_instance_hint_ref
-let add_instance_hint id = !add_instance_hint_ref id
-
-let remove_instance_hint_ref = ref (fun id -> assert false)
-let register_remove_instance_hint =
-  (:=) remove_instance_hint_ref
-let remove_instance_hint id = !remove_instance_hint_ref id
-
-let set_typeclass_transparency_ref = ref (fun id local c -> assert false)
-let register_set_typeclass_transparency =
-  (:=) set_typeclass_transparency_ref
-let set_typeclass_transparency gr local c = !set_typeclass_transparency_ref gr local c
-
-let classes_transparent_state_ref = ref (fun () -> assert false)
-let register_classes_transparent_state = (:=) classes_transparent_state_ref
-let classes_transparent_state () = !classes_transparent_state_ref ()
+let (add_instance_hint, add_instance_hint_hook) = Hook.make ()
+let add_instance_hint id = Hook.get add_instance_hint id
+
+let (remove_instance_hint, remove_instance_hint_hook) = Hook.make ()
+let remove_instance_hint id = Hook.get remove_instance_hint id
+
+let (set_typeclass_transparency, set_typeclass_transparency_hook) = Hook.make ()
+let set_typeclass_transparency gr local c = Hook.get set_typeclass_transparency gr local c
+
+let (classes_transparent_state, classes_transparent_state_hook) = Hook.make ()
+let classes_transparent_state () = Hook.get classes_transparent_state ()
 
 let solve_instanciation_problem = ref (fun _ _ _ -> assert false)
 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 46877a58f..c8f41841a 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -98,16 +98,16 @@ val resolve_typeclasses : ?filter:evar_filter -> ?split:bool -> ?fail:bool ->
   env -> evar_map -> evar_map
 val resolve_one_typeclass : env -> evar_map -> types -> open_constr
 
-val register_set_typeclass_transparency : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) -> unit
+val set_typeclass_transparency_hook : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) Hook.t
 val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
 
-val register_classes_transparent_state : (unit -> transparent_state) -> unit
+val classes_transparent_state_hook : (unit -> transparent_state) Hook.t
 val classes_transparent_state : unit -> transparent_state
 
-val register_add_instance_hint : 
-  (global_reference_or_constr -> global_reference list -> 
-   bool (* local? *) -> int option -> unit) -> unit
-val register_remove_instance_hint : (global_reference -> unit) -> unit
+val add_instance_hint_hook : 
+  (global_reference_or_constr -> global_reference list ->
+   bool (* local? *) -> int option -> unit) Hook.t
+val remove_instance_hint_hook : (global_reference -> unit) Hook.t
 val add_instance_hint : global_reference_or_constr -> global_reference list -> 
   bool -> int option -> unit
 val remove_instance_hint : global_reference -> unit
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index d57129ad3..37678525e 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -1014,13 +1014,13 @@ let pr_glob_tactic_level env =
 
 let pr_glob_tactic env = pr_glob_tactic_level env ltop
 
-let _ = Tactic_debug.set_tactic_printer
+let _ = Hook.set Tactic_debug.tactic_printer
   (fun x -> pr_glob_tactic (Global.env()) x)
 
-let _ = Tactic_debug.set_match_pattern_printer
+let _ = Hook.set Tactic_debug.match_pattern_printer
   (fun env hyp -> pr_match_pattern (pr_constr_pattern_env env) hyp)
 
-let _ = Tactic_debug.set_match_rule_printer
+let _ = Hook.set Tactic_debug.match_rule_printer
   (fun rl ->
     pr_match_rule false (pr_glob_tactic (Global.env()))
       (fun (_,p) -> pr_constr_pattern p) rl)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 90f20a738..cab86721f 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -69,9 +69,6 @@ let cook_proof hook =
   | (i,([e],cg,str,h)) -> (i,(e,cg,str,h))
   | _ -> Errors.anomaly ~label:"Pfedit.cook_proof" (Pp.str "more than one proof term.")
 
-let xml_cook_proof = ref (fun _ -> ())
-let set_xml_cook_proof f = xml_cook_proof := f
-
 let get_pftreestate () =
   Proof_global.give_me_the_proof ()
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 73850c6f0..976ac276e 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -95,9 +95,6 @@ val cook_proof : (Proof.proof -> unit) ->
     (Entries.definition_entry * lemma_possible_guards * goal_kind *
      unit declaration_hook)
 
-(** To export completed proofs to xml *)
-val set_xml_cook_proof : (goal_kind * Proof.proof -> unit) -> unit
-
 (** {6 ... } *)
 (** [get_pftreestate ()] returns the current focused pending proof.
    @raise NoCurrentProof if there is no pending proof. *)
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 8ad92910f..d73561f37 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -12,12 +12,9 @@ open Pp
 open Tacexpr
 open Termops
 
-let prtac = ref (fun _ -> assert false)
-let set_tactic_printer f = prtac := f
-let prmatchpatt = ref (fun _ _ -> assert false)
-let set_match_pattern_printer f = prmatchpatt := f
-let prmatchrl = ref (fun _ -> assert false)
-let set_match_rule_printer f = prmatchrl := f
+let (prtac, tactic_printer) = Hook.make ()
+let (prmatchpatt, match_pattern_printer) = Hook.make ()
+let (prmatchrl, match_rule_printer) = Hook.make ()
 
 (* This module intends to be a beginning of debugger for tactic expressions.
    Currently, it is quite simple and we can hope to have, in the future, a more
@@ -62,7 +59,7 @@ let help () =
 let goal_com g tac =
   begin
     db_pr_goal g;
-    msg_tac_debug (str "Going to execute:" ++ fnl () ++ !prtac tac)
+    msg_tac_debug (str "Going to execute:" ++ fnl () ++ Hook.get prtac tac)
   end
 
 let skipped = ref 0
@@ -164,7 +161,7 @@ let db_pattern_rule debug num r =
   if is_debug debug then
   begin
     msg_tac_debug (str "Pattern rule " ++ int num ++ str ":" ++ fnl () ++
-      str "|" ++ spc () ++ !prmatchrl r)
+      str "|" ++ spc () ++ Hook.get prmatchrl r)
   end
 
 (* Prints the hypothesis pattern identifier if it exists *)
@@ -195,7 +192,7 @@ let db_hyp_pattern_failure debug env (na,hyp) =
   if is_debug debug then
     msg_tac_debug (str ("The pattern hypothesis"^(hyp_bound na)^
                 " cannot match: ") ++
-           !prmatchpatt env hyp)
+           Hook.get prmatchpatt env hyp)
 
 (* Prints a matching failure message for a rule *)
 let db_matching_failure debug =
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 8afee3418..a9cd025a7 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -18,12 +18,11 @@ open Term
    Currently, it is quite simple and we can hope to have, in the future, a more
    complete panel of commands dedicated to a proof assistant framework *)
 
-val set_tactic_printer : (glob_tactic_expr -> Pp.std_ppcmds) -> unit
-val set_match_pattern_printer :
-  (env -> constr_pattern match_pattern -> Pp.std_ppcmds) -> unit
-val set_match_rule_printer :
-  ((Genarg.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) ->
-    unit
+val tactic_printer : (glob_tactic_expr -> Pp.std_ppcmds) Hook.t
+val match_pattern_printer :
+  (env -> constr_pattern match_pattern -> Pp.std_ppcmds) Hook.t
+val match_rule_printer :
+  ((Genarg.glob_constr_and_expr * constr_pattern,glob_tactic_expr) match_rule -> Pp.std_ppcmds) Hook.t
 
 (** Debug information *)
 type debug_info =
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 5aab5f252..f12bddfb7 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -643,10 +643,7 @@ let cache_autohint (_,(local,name,hints)) =
   | RemoveHints grs -> remove_hint name grs
   | AddCut path -> add_cut name path
 
-let forward_subst_tactic =
-  ref (fun _ -> failwith "subst_tactic is not installed for auto")
-
-let set_extern_subst_tactic f = forward_subst_tactic := f
+let (forward_subst_tactic, extern_subst_tactic) = Hook.make ()
 
 let subst_autohint (subst,(local,name,hintlist as obj)) =
   let subst_key gr =
@@ -679,7 +676,7 @@ let subst_autohint (subst,(local,name,hintlist as obj)) =
           let ref' = subst_evaluable_reference subst ref in
           if ref==ref' then data.code else Unfold_nth ref'
       | Extern tac ->
-	  let tac' = !forward_subst_tactic subst tac in
+	  let tac' = Hook.get forward_subst_tactic subst tac in
 	  if tac==tac' then data.code else Extern tac'
     in
     let name' = subst_path_atom subst data.name in
@@ -793,10 +790,7 @@ let add_trivials env sigma l local dbnames =
 		    AddHints (List.map (fun (name, c) -> make_trivial env sigma ~name c) l))))
     dbnames
 
-let forward_intern_tac =
-  ref (fun _ -> failwith "intern_tac is not installed for auto")
-
-let set_extern_intern_tac f = forward_intern_tac := f
+let (forward_intern_tac, extern_intern_tac) = Hook.make ()
 
 type hints_entry =
   | HintsResolveEntry of (int option * bool * hints_path_atom * global_reference_or_constr) list
@@ -880,7 +874,8 @@ let interp_hints =
 	HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid))
   | HintsExtern (pri, patcom, tacexp) ->
       let pat =	Option.map fp patcom in
-      let tacexp = !forward_intern_tac (match pat with None -> [] | Some (l, _) -> l) tacexp in
+      let l = match pat with None -> [] | Some (l, _) -> l in
+      let tacexp = Hook.get forward_intern_tac l tacexp in
       HintsExternEntry (pri, pat, tacexp)
 
 let add_hints local dbnames0 h =
@@ -1104,10 +1099,7 @@ si après Intros la conclusion matche le pattern.
 
 (* conclPattern doit échouer avec error car il est rattraper par tclFIRST *)
 
-let forward_interp_tactic =
-  ref (fun _ -> failwith "interp_tactic is not installed for auto")
-
-let set_extern_interp f = forward_interp_tactic := f
+let (forward_interp_tactic, extern_interp) = Hook.make ()
 
 let conclPattern concl pat tac gl =
   let constr_bindings =
@@ -1116,7 +1108,7 @@ let conclPattern concl pat tac gl =
     | Some pat ->
 	try matches pat concl
 	with PatternMatchingFailure -> error "conclPattern" in
-    !forward_interp_tactic constr_bindings tac gl
+    Hook.get forward_interp_tactic constr_bindings tac gl
 
 (***********************************************************)
 (** A debugging / verbosity framework for trivial and auto *)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 99f4768c2..2a163120a 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -173,16 +173,14 @@ val make_extern :
   int -> constr_pattern option -> Tacexpr.glob_tactic_expr
       -> hint_entry
 
-val set_extern_interp :
-  (patvar_map -> Tacexpr.glob_tactic_expr -> tactic) -> unit
+val extern_interp :
+  (patvar_map -> Tacexpr.glob_tactic_expr -> tactic) Hook.t
 
-val set_extern_intern_tac :
-  (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr)
-  -> unit
+val extern_intern_tac :
+  (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t
 
-val set_extern_subst_tactic :
-  (substitution -> Tacexpr.glob_tactic_expr -> Tacexpr.glob_tactic_expr)
-  -> unit
+val extern_subst_tactic :
+  (substitution -> Tacexpr.glob_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t
 
 (** Create a Hint database from the pairs (name, constr).
    Useful to take the current goal hypotheses as hints;
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 2dc42e35f..b0bcf57d7 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -228,11 +228,8 @@ let general_elim_clause with_evars frzevars tac cls sigma c t l l2r elim gl =
   If occurrences are set, use general rewrite.
 *)
 
-let general_rewrite_clause = ref (fun _ -> assert false)
-let register_general_rewrite_clause = (:=) general_rewrite_clause
-
-let is_applied_rewrite_relation = ref (fun _ _ _ _ -> None)
-let register_is_applied_rewrite_relation = (:=) is_applied_rewrite_relation
+let (forward_general_rewrite_clause, general_rewrite_clause) = Hook.make ()
+let (forward_is_applied_rewrite_relation, is_applied_rewrite_relation) = Hook.make ()
 
 (* Do we have a JMeq instance on twice the same domains ? *)
 
@@ -331,7 +328,7 @@ let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac)
 let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
     ((c,l) : constr with_bindings) with_evars gl =
   if occs != AllOccurrences then (
-    rewrite_side_tac (!general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac gl)
+    rewrite_side_tac (Hook.get forward_general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac gl)
   else
     let env = pf_env gl in
     let sigma = project gl in
@@ -344,7 +341,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
 	    l with_evars frzevars dep_proof_ok gl hdcncl
       | None ->
 	  try
-	    rewrite_side_tac (!general_rewrite_clause cls
+	    rewrite_side_tac (Hook.get forward_general_rewrite_clause cls
 				 lft2rgt occs (c,l) ~new_goals:[]) tac gl
 	  with e when Errors.noncritical e ->
             (* Try to see if there's an equality hidden *)
@@ -1562,7 +1559,8 @@ let replace_multi_term dir_opt c  =
   in
   rewrite_multi_assumption_cond cond_eq_fun
 
-let _ = Tactics.register_general_multi_rewrite
-  (fun b evars t cls -> general_multi_rewrite b evars t cls)
+let _ =
+  let gmr l2r with_evars tac c = general_multi_rewrite l2r with_evars tac c in
+  Hook.set Tactics.general_multi_rewrite gmr
 
-let _ = Tactics.register_subst_one (fun b -> subst_one b)
+let _ = Hook.set Tactics.subst_one subst_one
diff --git a/tactics/equality.mli b/tactics/equality.mli
index aa1bfaa0f..147218efd 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -51,10 +51,10 @@ val rewriteRL : ?tac:(tactic * conditions) -> constr  -> tactic
 
 (* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *)
 
-val register_general_rewrite_clause :
+val general_rewrite_clause :
   (Id.t option -> orientation ->
-    occurrences -> constr with_bindings -> new_goals:constr list -> tactic) -> unit
-val register_is_applied_rewrite_relation : (env -> evar_map -> rel_context -> constr -> constr option) -> unit
+    occurrences -> constr with_bindings -> new_goals:constr list -> tactic) Hook.t
+val is_applied_rewrite_relation : (env -> evar_map -> rel_context -> constr -> constr option) Hook.t
 
 val general_rewrite_ebindings_clause : Id.t option ->
   orientation -> occurrences -> freeze_evars_flag -> dep_proof_flag ->
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 5722c11ea..0e6654545 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -123,7 +123,7 @@ let is_applied_rewrite_relation env sigma rels t =
   | _ -> None
 
 let _ =
-  Equality.register_is_applied_rewrite_relation is_applied_rewrite_relation
+  Hook.set Equality.is_applied_rewrite_relation is_applied_rewrite_relation
 
 let split_head = function
     hd :: tl -> hd, tl
@@ -1970,7 +1970,7 @@ let general_s_rewrite_clause x =
     | None -> general_s_rewrite None
     | Some id -> general_s_rewrite (Some id)
 
-let _ = Equality.register_general_rewrite_clause general_s_rewrite_clause
+let _ = Hook.set Equality.general_rewrite_clause general_s_rewrite_clause
 
 (** [setoid_]{reflexivity,symmetry,transitivity} tactics *)
 
@@ -2032,10 +2032,10 @@ let setoid_symmetry_in id gl =
 	tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ] ]
       gl
 
-let _ = Tactics.register_setoid_reflexivity setoid_reflexivity
-let _ = Tactics.register_setoid_symmetry setoid_symmetry
-let _ = Tactics.register_setoid_symmetry_in setoid_symmetry_in
-let _ = Tactics.register_setoid_transitivity setoid_transitivity
+let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
+let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry
+let _ = Hook.set Tactics.setoid_symmetry_in setoid_symmetry_in
+let _ = Hook.set Tactics.setoid_transitivity setoid_transitivity
 
 TACTIC EXTEND setoid_symmetry
    [ "setoid_symmetry" ] -> [ setoid_symmetry ]
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 6a1a33fb0..b7108f4d3 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -983,7 +983,8 @@ let add_tacdef local isrec tacl =
 (***************************************************************************)
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
 
-let _ = Auto.set_extern_intern_tac
-  (fun l ->
-    Flags.with_option strict_check
-    (intern_pure_tactic { (make_empty_glob_sign()) with ltacvars=(l,[])}))
+let _ =
+  let f l = Flags.with_option strict_check
+    (intern_pure_tactic { (make_empty_glob_sign()) with ltacvars=(l,[])})
+  in
+  Hook.set Auto.extern_intern_tac f
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index da0a3c7d9..26f7d02b9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -2023,7 +2023,7 @@ let tacticIn t =
 (***************************************************************************)
 (* Backwarding recursive needs of tactic glob/interp/eval functions *)
 
-let _ = Auto.set_extern_interp
+let _ = Hook.set Auto.extern_interp
   (fun l ->
     let l = List.map (fun (id,c) -> (id,VConstr ([],c))) l in
     interp_tactic {lfun=l;avoid_ids=[];debug=get_debug(); trace=[]})
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index 90739a4e9..1cf4264ea 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -347,4 +347,4 @@ and subst_genarg subst (x:glob_generic_argument) =
       | None ->
           lookup_genarg_subst s subst x
 
-let _ = Auto.set_extern_subst_tactic subst_tactic
+let _ = Hook.set Auto.extern_subst_tactic subst_tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0599c52d1..ab962a4cc 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1286,18 +1286,10 @@ let simplest_split = split NoBindings
 (*****************************)
 
 (* Rewriting function for rewriting one hypothesis at the time *)
-let forward_general_multi_rewrite =
-  ref (fun _ -> failwith "general_multi_rewrite undefined")
+let (forward_general_multi_rewrite, general_multi_rewrite) = Hook.make ()
 
 (* Rewriting function for substitution (x=t) everywhere at the same time *)
-let forward_subst_one =
-  ref (fun _ -> failwith "subst_one undefined")
-
-let register_general_multi_rewrite f =
-  forward_general_multi_rewrite := f
-
-let register_subst_one f =
-  forward_subst_one := f
+let (forward_subst_one, subst_one) = Hook.make ()
 
 let error_unexpected_extra_pattern loc nb pat =
   let s1,s2,s3 = match pat with
@@ -1331,9 +1323,9 @@ let intro_or_and_pattern loc b ll l' tac id gl =
 
 let rewrite_hyp l2r id gl =
   let rew_on l2r =
-    !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) in
+    Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) in
   let subst_on l2r x rhs =
-    !forward_subst_one true x (id,rhs,l2r) in
+    Hook.get forward_subst_one true x (id,rhs,l2r) in
   let clear_var_and_eq c =
     tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in
   let t = pf_whd_betadeltaiota gl (pf_type_of gl (mkVar id)) in
@@ -1444,7 +1436,7 @@ let prepare_intros s ipat gl = match ipat with
   | IntroWildcard -> let id = make_id s gl in id, clear_wildcards [dloc,id]
   | IntroRewrite l2r ->
       let id = make_id s gl in
-      id, !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
+      id, Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
   | IntroOrAndPattern ll -> make_id s gl,
       onLastHypId
 	(intro_or_and_pattern loc true ll []
@@ -1479,7 +1471,7 @@ let assert_tac na = assert_as true (ipat_of_name na)
 
 let as_tac id ipat = match ipat with
   | Some (loc,IntroRewrite l2r) ->
-      !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
+      Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
   | Some (loc,IntroOrAndPattern ll) ->
       intro_or_and_pattern loc true ll []
         (intros_patterns true [] [] [] MoveLast (fun _ -> clear_wildcards))
@@ -3371,8 +3363,7 @@ let dImp cls =
 
 (* Reflexivity tactics *)
 
-let setoid_reflexivity = ref (fun _ -> assert false)
-let register_setoid_reflexivity f = setoid_reflexivity := f
+let (forward_setoid_reflexivity, setoid_reflexivity) = Hook.make ()
 
 let reflexivity_red allowred gl =
   (* PL: usual reflexivity don't perform any reduction when searching
@@ -3386,7 +3377,8 @@ let reflexivity_red allowred gl =
     | Some _ -> one_constructor 1 NoBindings gl
 
 let reflexivity gl =
-  try reflexivity_red false gl with NoEquationFound -> !setoid_reflexivity gl
+  try reflexivity_red false gl
+  with NoEquationFound -> Hook.get forward_setoid_reflexivity gl
 
 let intros_reflexivity  = (tclTHEN intros reflexivity)
 
@@ -3397,8 +3389,7 @@ let intros_reflexivity  = (tclTHEN intros reflexivity)
    defined and the conclusion is a=b, it solves the goal doing (Cut
    b=a;Intro H;Case H;Constructor 1) *)
 
-let setoid_symmetry = ref (fun _ -> assert false)
-let register_setoid_symmetry f = setoid_symmetry := f
+let (forward_setoid_symmetry, setoid_symmetry) = Hook.make ()
 
 (* This is probably not very useful any longer *)
 let prove_symmetry hdcncl eq_kind =
@@ -3428,10 +3419,9 @@ let symmetry_red allowred gl =
   | None,eq,eq_kind -> prove_symmetry eq eq_kind gl
 
 let symmetry gl =
-  try symmetry_red false gl with NoEquationFound -> !setoid_symmetry gl
+  try symmetry_red false gl with NoEquationFound -> Hook.get forward_setoid_symmetry gl
 
-let setoid_symmetry_in = ref (fun _ _ -> assert false)
-let register_setoid_symmetry_in f = setoid_symmetry_in := f
+let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make ()
 
 let symmetry_in id gl =
   let ctype = pf_type_of gl (mkVar id) in
@@ -3446,7 +3436,7 @@ let symmetry_in id gl =
       [ intro_replacing id;
         tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ]
       gl
-  with NoEquationFound -> !setoid_symmetry_in id gl
+  with NoEquationFound -> Hook.get forward_setoid_symmetry_in id gl
 
 let intros_symmetry =
   onClause
@@ -3466,8 +3456,7 @@ let intros_symmetry =
    --Eduardo (19/8/97)
 *)
 
-let setoid_transitivity = ref (fun _ _ -> assert false)
-let register_setoid_transitivity f = setoid_transitivity := f
+let (forward_setoid_transitivity, setoid_transitivity) = Hook.make ()
 
 (* This is probably not very useful any longer *)
 let prove_transitivity hdcncl eq_kind t gl =
@@ -3509,7 +3498,7 @@ let transitivity_red allowred t gl =
 
 let transitivity_gen t gl =
   try transitivity_red false t gl
-  with NoEquationFound -> !setoid_transitivity t gl
+  with NoEquationFound -> Hook.get forward_setoid_transitivity t gl
 
 let etransitivity = transitivity_gen None
 let transitivity t = transitivity_gen (Some t)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 2b45ecde6..7c0fee5c7 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -337,19 +337,19 @@ val simplest_split       : tactic
 
 (** {6 Logical connective tactics. } *)
 
-val register_setoid_reflexivity : tactic -> unit
+val setoid_reflexivity          : tactic Hook.t
 val reflexivity_red             : bool -> tactic
 val reflexivity                 : tactic
 val intros_reflexivity          : tactic
 
-val register_setoid_symmetry : tactic -> unit
+val setoid_symmetry             : tactic Hook.t
 val symmetry_red                : bool -> tactic
 val symmetry                    : tactic
-val register_setoid_symmetry_in : (Id.t -> tactic) -> unit
+val setoid_symmetry_in          : (Id.t -> tactic) Hook.t
 val symmetry_in                 : Id.t -> tactic
 val intros_symmetry             : clause -> tactic
 
-val register_setoid_transitivity : (constr option -> tactic) -> unit
+val setoid_transitivity         : (constr option -> tactic) Hook.t
 val transitivity_red            : bool -> constr option -> tactic
 val transitivity                : constr -> tactic
 val etransitivity               : tactic
@@ -385,8 +385,8 @@ val admit_as_an_axiom : tactic
 val abstract_generalize : ?generalize_vars:bool -> ?force_dep:bool -> Id.t -> tactic
 val specialize_eqs : Id.t -> tactic
 
-val register_general_multi_rewrite :
-  (bool -> evars_flag -> constr with_bindings -> clause -> tactic) -> unit
+val general_multi_rewrite :
+  (bool -> evars_flag -> constr with_bindings -> clause -> tactic) Hook.t
 
-val register_subst_one :
-  (bool -> Id.t -> Id.t * constr * bool -> tactic) -> unit
+val subst_one :
+  (bool -> Id.t -> Id.t * constr * bool -> tactic) Hook.t
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 9fc5d0278..3f56f80dc 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -35,14 +35,14 @@ let set_typeclass_transparency c local b =
     (Auto.HintsTransparencyEntry ([c], b))
     
 let _ =
-  Typeclasses.register_add_instance_hint
+  Hook.set Typeclasses.add_instance_hint_hook
     (fun inst path local pri ->
       Flags.silently (fun () ->
 	Auto.add_hints local [typeclasses_db]
 	  (Auto.HintsResolveEntry
 	     [pri, false, Auto.PathHints path, inst])) ());
-  Typeclasses.register_set_typeclass_transparency set_typeclass_transparency;
-  Typeclasses.register_classes_transparent_state 
+  Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
+  Hook.set Typeclasses.classes_transparent_state_hook
     (fun () -> Auto.Hint_db.transparent_state (Auto.searchtable_map typeclasses_db))
     
 let declare_class g =
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 67bc387ab..369abd3f8 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -204,15 +204,11 @@ let declare_assumption is_coe (local,kind) c imps impl nl (_,ident) = match loca
   let () = if is_coe then Class.try_add_new_coercion gr local in
   (gr,Lib.is_modtype_strict ())
 
-let declare_assumptions_hook = ref ignore
-let set_declare_assumptions_hook = (:=) declare_assumptions_hook
-
 let interp_assumption evdref env bl c =
   let c = prod_constr_expr c bl in
   interp_type_evars_impls evdref env c
 
 let declare_assumptions idl is_coe k c imps impl_is_on nl =
-  !declare_assumptions_hook c;
   let refs, status =
     List.fold_left (fun (refs,status) id ->
       let ref',status' = declare_assumption is_coe k c imps impl_is_on nl id in
diff --git a/toplevel/command.mli b/toplevel/command.mli
index f38d954a1..71eec3295 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -27,7 +27,6 @@ open Pfedit
 
 val set_declare_definition_hook : (definition_entry -> unit) -> unit
 val get_declare_definition_hook : unit -> (definition_entry -> unit)
-val set_declare_assumptions_hook : (types -> unit) -> unit
 
 (** {6 Definitions/Let} *)
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 14e4b8eb7..fcffb343e 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -399,11 +399,8 @@ let eval_expr ?(preserving=false) loc_ast =
     Backtrack.mark_command (snd loc_ast)
 
 (* XML output hooks *)
-let xml_start_library = ref (fun _ -> ())
-let xml_end_library = ref (fun _ -> ())
-
-let set_xml_start_library f = xml_start_library := f
-let set_xml_end_library f = xml_end_library := f
+let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore ()
+let (f_xml_end_library, xml_end_library) = Hook.make ~default:ignore ()
 
 (* Load a vernac file. Errors are annotated with file and location *)
 let load_vernac verb file =
@@ -423,11 +420,11 @@ let compile verbosely f =
   let ldir,long_f_dot_v = Flags.verbosely Library.start_library f in
   Dumpglob.start_dump_glob long_f_dot_v;
   Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
-  if !Flags.xml_export then !xml_start_library ();
+  if !Flags.xml_export then Hook.get f_xml_start_library ();
   let _ = load_vernac verbosely long_f_dot_v in
   let pfs = Pfedit.get_all_proof_names () in
   if not (List.is_empty pfs) then
     (pperrnl (str "Error: There are pending proofs"); flush_all (); exit 1);
-  if !Flags.xml_export then !xml_end_library ();
+  if !Flags.xml_export then Hook.get f_xml_end_library ();
   Library.save_library_to ldir (long_f_dot_v ^ "o");
   Dumpglob.end_dump_glob ()
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 379194945..bda42dfa6 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -29,8 +29,8 @@ val just_parsing : bool ref
 val eval_expr : ?preserving:bool -> Loc.t * Vernacexpr.vernac_expr -> unit
 
 (** Set XML hooks *)
-val set_xml_start_library : (unit -> unit) -> unit
-val set_xml_end_library   : (unit -> unit) -> unit
+val xml_start_library : (unit -> unit) Hook.t
+val xml_end_library   : (unit -> unit) Hook.t
 
 (** Load a vernac file, verbosely or not. Errors are annotated with file
    and location *)