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

1 files changed, 3 insertions, 6 deletions

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 *)