From de26e97cf37cafd37b83377d2df062a6e82676e7 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sun, 12 May 2013 15:33:40 +0000
Subject: 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
---
 plugins/extraction/extraction.ml | 2 +-
 plugins/extraction/table.ml      | 5 ++---
 plugins/extraction/table.mli     | 2 +-
 3 files changed, 4 insertions(+), 5 deletions(-)

(limited to 'plugins/extraction')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index a6a9838ae8..5c67c33b6a 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 ebe7230ec2..5817357362 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 53acccf843..ce6f8e229e 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
-- 
cgit v1.2.3