diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/dp/dp.ml | 12 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 17 | ||||
| -rw-r--r-- | plugins/field/field.ml4 | 2 | ||||
| -rw-r--r-- | plugins/funind/indfun_common.ml | 2 | ||||
| -rw-r--r-- | plugins/ring/ring.ml | 2 | ||||
| -rw-r--r-- | plugins/setoid_ring/newring.ml4 | 4 | ||||
| -rw-r--r-- | plugins/subtac/subtac_obligations.ml | 2 |
7 files changed, 20 insertions, 21 deletions
diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml index b025cea64a..837195e44f 100644 --- a/plugins/dp/dp.ml +++ b/plugins/dp/dp.ml @@ -36,7 +36,7 @@ let set_trace b = trace := b let timeout = ref 10 let set_timeout n = timeout := n -let dp_timeout_obj = +let dp_timeout_obj : int -> obj = declare_object {(default_object "Dp_timeout") with cache_function = (fun (_,x) -> set_timeout x); @@ -44,7 +44,7 @@ let dp_timeout_obj = let dp_timeout x = Lib.add_anonymous_leaf (dp_timeout_obj x) -let dp_debug_obj = +let dp_debug_obj : bool -> obj = declare_object {(default_object "Dp_debug") with cache_function = (fun (_,x) -> set_debug x); @@ -52,7 +52,7 @@ let dp_debug_obj = let dp_debug x = Lib.add_anonymous_leaf (dp_debug_obj x) -let dp_trace_obj = +let dp_trace_obj : bool -> obj = declare_object {(default_object "Dp_trace") with cache_function = (fun (_,x) -> set_trace x); @@ -825,7 +825,7 @@ let prelude_files = ref ([] : string list) let set_prelude l = prelude_files := l -let dp_prelude_obj = +let dp_prelude_obj : string list -> obj = declare_object {(default_object "Dp_prelude") with cache_function = (fun (_,x) -> set_prelude x); @@ -1087,7 +1087,7 @@ let dp_hint l = in List.iter one_hint (List.map (fun qid -> qid, Nametab.global qid) l) -let dp_hint_obj = +let dp_hint_obj : reference list -> obj = declare_object {(default_object "Dp_hint") with cache_function = (fun (_,l) -> dp_hint l); @@ -1113,7 +1113,7 @@ let dp_predefined qid s = with NotFO -> msg_warning (str " ignored (not a first order declaration)") -let dp_predefined_obj = +let dp_predefined_obj : reference * string -> obj = declare_object {(default_object "Dp_predefined") with cache_function = (fun (_,(id,s)) -> dp_predefined id s); diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 502d062353..75584ead38 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); diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4 index 8b6bb133a1..9e4f4d7452 100644 --- a/plugins/field/field.ml4 +++ b/plugins/field/field.ml4 @@ -67,7 +67,7 @@ let subst_addfield (subst,(typ,th as obj)) = (typ',th') (* Declaration of the Add Field library object *) -let in_addfield = +let in_addfield : types * constr -> Libobject.obj = Libobject.declare_object {(Libobject.default_object "ADD_FIELD") with Libobject.open_function = (fun i o -> if i=1 then cache_addfield o); Libobject.cache_function = cache_addfield; diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 094d2e50fd..951b25baf2 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -362,7 +362,7 @@ let pr_table tb = let l = Cmap.fold (fun k v acc -> v::acc) tb [] in Util.prlist_with_sep fnl pr_info l -let in_Function = +let in_Function : function_info -> Libobject.obj = Libobject.declare_object {(Libobject.default_object "FUNCTIONS_DB") with Libobject.cache_function = cache_Function; diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml index 9a252dfb71..98d6361c0d 100644 --- a/plugins/ring/ring.ml +++ b/plugins/ring/ring.ml @@ -262,7 +262,7 @@ let subst_th (subst,(c,th as obj)) = (c',th') -let theory_to_obj = +let theory_to_obj : constr * theory -> obj = let cache_th (_,(c, th)) = theories_map_add (c,th) in declare_object {(default_object "tactic-ring-theory") with open_function = (fun i o -> if i=1 then cache_th o); diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4 index 6ff6730235..af236bc0ff 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -438,7 +438,7 @@ let subst_th (subst,th) = ring_post_tac = posttac' } -let theory_to_obj = +let theory_to_obj : ring_info -> obj = let cache_th (name,th) = add_entry name th in declare_object {(default_object "tactic-new-ring-theory") with @@ -1014,7 +1014,7 @@ let subst_th (subst,th) = field_pre_tac = pretac'; field_post_tac = posttac' } -let ftheory_to_obj = +let ftheory_to_obj : field_info -> obj = let cache_th (name,th) = add_field_entry name th in declare_object {(default_object "tactic-new-field-theory") with diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml index b3ff7c9f00..74ee05bbc6 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -213,7 +213,7 @@ let close sec = (str (if List.length keys = 1 then " has " else "have ") ++ str "unsolved obligations")) -let input = +let input : program_info ProgMap.t -> obj = declare_object { (default_object "Program state") with cache_function = (fun (na, pi) -> from_prg := pi); |