Add type annotations around all calls to Libobject.declare_object

 These annotations are purely optional, but could be quite helpful
 when trying to understand the code, and in particular trying to
 trace which which data-structure may end in the libobject part
 of a vo. By the way, we performed some code simplifications :
  - in Library, a part of the REQUIRE objects was unused.
  - in Declaremods, we removed some checks that were marked as
  useless, this allows to slightly simplify the stored objects.

 To investigate someday : in recordops, the RECMETHODS is storing
 some evar_maps. This is ok for the moment, but might not be in
 the future (cf previous commit on auto hints). This RECMETHODS
 was not detected by my earlier tests : not used in the stdlib ?

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

1 files changed, 8 insertions, 9 deletions

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 502d06235..75584ead3 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -493,7 +493,7 @@ let lang_ref = ref Ocaml
 
 let lang () = !lang_ref
 
-let extr_lang =
+let extr_lang : lang -> obj =
   declare_object
     {(default_object "Extraction Lang") with
        cache_function = (fun (_,l) -> lang_ref := l);
@@ -525,7 +525,7 @@ let add_inline_entries b l =
 
 (* Registration of operations for rollback. *)
 
-let inline_extraction =
+let inline_extraction : bool * global_reference list -> obj =
   declare_object
     {(default_object "Extraction Inline") with
        cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
@@ -569,7 +569,7 @@ let print_extraction_inline () =
 
 (* Reset part *)
 
-let reset_inline =
+let reset_inline : unit -> obj =
   declare_object
     {(default_object "Reset Extraction Inline") with
        cache_function = (fun (_,_)-> inline_table :=  empty_inline_table);
@@ -608,7 +608,7 @@ let add_implicits r l =
 
 (* Registration of operations for rollback. *)
 
-let implicit_extraction =
+let implicit_extraction : global_reference * int_or_id list -> obj =
   declare_object
     {(default_object "Extraction Implicit") with
        cache_function = (fun (_,(r,l)) -> add_implicits r l);
@@ -668,12 +668,11 @@ let add_blacklist_entries l =
 
 (* Registration of operations for rollback. *)
 
-let blacklist_extraction =
+let blacklist_extraction : string list -> obj =
   declare_object
     {(default_object "Extraction Blacklist") with
        cache_function = (fun (_,l) -> add_blacklist_entries l);
        load_function = (fun _ (_,l) -> add_blacklist_entries l);
-       classify_function = (fun o -> Libobject.Keep o);
        subst_function = (fun (_,x) -> x)
     }
 
@@ -696,7 +695,7 @@ let print_extraction_blacklist () =
 
 (* Reset part *)
 
-let reset_blacklist =
+let reset_blacklist : unit -> obj =
   declare_object
     {(default_object "Reset Extraction Blacklist") with
        cache_function = (fun (_,_)-> blacklist_table := Idset.empty);
@@ -742,7 +741,7 @@ let find_custom_match pv =
 
 (* Registration of operations for rollback. *)
 
-let in_customs =
+let in_customs : global_reference * string list * string -> obj =
   declare_object
     {(default_object "ML extractions") with
        cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
@@ -757,7 +756,7 @@ let _ = declare_summary "ML extractions"
 	    unfreeze_function = ((:=) customs);
 	    init_function = (fun () -> customs := Refmap'.empty) }
 
-let in_custom_matchs =
+let in_custom_matchs : global_reference * string -> obj =
   declare_object
     {(default_object "ML extractions custom matchs") with
        cache_function = (fun (_,(r,s)) -> add_custom_match r s);