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

5 files changed, 9 insertions, 17 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 9fc5d02787..3f56f80dc8 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 67bc387abe..369abd3f87 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 f38d954a17..71eec32958 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 14e4b8eb7d..fcffb343ee 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 3791949459..bda42dfa62 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 *)