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

4 files changed, 13 insertions, 19 deletions

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