From b359ef0ffad7fd1fc0e4db99fc1e38a1389802bc Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 2 Nov 2011 18:59:57 +0000 Subject: 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 --- plugins/extraction/table.ml | 17 ++++++++--------- 1 file changed, 8 insertions(+), 9 deletions(-) (limited to 'plugins/extraction') 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); -- cgit v1.2.3