diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/dp/dp.ml | 12 | ||||
| -rw-r--r-- | plugins/extraction/table.ml | 16 | ||||
| -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, 20 deletions
diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml index 34b32c0a7a..b800170de3 100644 --- a/plugins/dp/dp.ml +++ b/plugins/dp/dp.ml @@ -37,7 +37,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 = declare_object {(default_object "Dp_timeout") with cache_function = (fun (_,x) -> set_timeout x); @@ -45,7 +45,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 = declare_object {(default_object "Dp_debug") with cache_function = (fun (_,x) -> set_debug x); @@ -53,7 +53,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 = declare_object {(default_object "Dp_trace") with cache_function = (fun (_,x) -> set_trace x); @@ -826,7 +826,7 @@ let prelude_files = ref ([] : string list) let set_prelude l = prelude_files := l -let (dp_prelude_obj,_) = +let dp_prelude_obj = declare_object {(default_object "Dp_prelude") with cache_function = (fun (_,x) -> set_prelude x); @@ -1088,7 +1088,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 = declare_object {(default_object "Dp_hint") with cache_function = (fun (_,l) -> dp_hint l); @@ -1114,7 +1114,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 = 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 5457d2e8c2..a292dec2f9 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -459,7 +459,7 @@ let lang_ref = ref Ocaml let lang () = !lang_ref -let (extr_lang,_) = +let extr_lang = declare_object {(default_object "Extraction Lang") with cache_function = (fun (_,l) -> lang_ref := l); @@ -491,7 +491,7 @@ let add_inline_entries b l = (* Registration of operations for rollback. *) -let (inline_extraction,_) = +let inline_extraction = declare_object {(default_object "Extraction Inline") with cache_function = (fun (_,(b,l)) -> add_inline_entries b l); @@ -534,7 +534,7 @@ let print_extraction_inline () = (* Reset part *) -let (reset_inline,_) = +let reset_inline = declare_object {(default_object "Reset Extraction Inline") with cache_function = (fun (_,_)-> inline_table := empty_inline_table); @@ -573,7 +573,7 @@ let add_implicits r l = (* Registration of operations for rollback. *) -let (implicit_extraction,_) = +let implicit_extraction = declare_object {(default_object "Extraction Implicit") with cache_function = (fun (_,(r,l)) -> add_implicits r l); @@ -633,7 +633,7 @@ let add_blacklist_entries l = (* Registration of operations for rollback. *) -let (blacklist_extraction,_) = +let blacklist_extraction = declare_object {(default_object "Extraction Blacklist") with cache_function = (fun (_,l) -> add_blacklist_entries l); @@ -661,7 +661,7 @@ let print_extraction_blacklist () = (* Reset part *) -let (reset_blacklist,_) = +let reset_blacklist = declare_object {(default_object "Reset Extraction Blacklist") with cache_function = (fun (_,_)-> blacklist_table := Idset.empty); @@ -707,7 +707,7 @@ let find_custom_match pv = (* Registration of operations for rollback. *) -let (in_customs,_) = +let in_customs = declare_object {(default_object "ML extractions") with cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s); @@ -722,7 +722,7 @@ let _ = declare_summary "ML extractions" unfreeze_function = ((:=) customs); init_function = (fun () -> customs := Refmap'.empty) } -let (in_custom_matchs,_) = +let in_custom_matchs = 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 d4ced4139a..1cba563eaf 100644 --- a/plugins/field/field.ml4 +++ b/plugins/field/field.ml4 @@ -65,7 +65,7 @@ let subst_addfield (subst,(typ,th as obj)) = (typ',th') (* Declaration of the Add Field library object *) -let (in_addfield,out_addfield)= +let in_addfield = 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 ff7089613f..002fb70986 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,out_Function = +let in_Function = 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 8b977e5dce..7588e6a2fa 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, obj_to_theory) = +let theory_to_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 fa0e76841a..052406867d 100644 --- a/plugins/setoid_ring/newring.ml4 +++ b/plugins/setoid_ring/newring.ml4 @@ -440,7 +440,7 @@ let subst_th (subst,th) = ring_post_tac = posttac' } -let (theory_to_obj, obj_to_theory) = +let theory_to_obj = let cache_th (name,th) = add_entry name th in declare_object {(default_object "tactic-new-ring-theory") with @@ -1016,7 +1016,7 @@ let subst_th (subst,th) = field_pre_tac = pretac'; field_post_tac = posttac' } -let (ftheory_to_obj, obj_to_ftheory) = +let ftheory_to_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 591e01c04e..22cc745f6d 100644 --- a/plugins/subtac/subtac_obligations.ml +++ b/plugins/subtac/subtac_obligations.ml @@ -153,7 +153,7 @@ let _ = let progmap_union = ProgMap.fold ProgMap.add -let (input,output) = +let input = declare_object { (default_object "Program state") with classify_function = (fun () -> |