diff options
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 17 |
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); |