aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/dp/dp.ml18
-rw-r--r--plugins/extraction/table.ml12
-rw-r--r--plugins/field/field.ml44
-rw-r--r--plugins/funind/indfun_common.ml3
-rw-r--r--plugins/ring/ring.ml8
-rw-r--r--plugins/setoid_ring/newring.ml416
-rw-r--r--plugins/subtac/subtac_obligations.ml3
7 files changed, 20 insertions, 44 deletions
diff --git a/plugins/dp/dp.ml b/plugins/dp/dp.ml
index dc4698c5ea..6365043611 100644
--- a/plugins/dp/dp.ml
+++ b/plugins/dp/dp.ml
@@ -40,8 +40,7 @@ let (dp_timeout_obj,_) =
declare_object
{(default_object "Dp_timeout") with
cache_function = (fun (_,x) -> set_timeout x);
- load_function = (fun _ (_,x) -> set_timeout x);
- export_function = (fun x -> Some x)}
+ load_function = (fun _ (_,x) -> set_timeout x)}
let dp_timeout x = Lib.add_anonymous_leaf (dp_timeout_obj x)
@@ -49,8 +48,7 @@ let (dp_debug_obj,_) =
declare_object
{(default_object "Dp_debug") with
cache_function = (fun (_,x) -> set_debug x);
- load_function = (fun _ (_,x) -> set_debug x);
- export_function = (fun x -> Some x)}
+ load_function = (fun _ (_,x) -> set_debug x)}
let dp_debug x = Lib.add_anonymous_leaf (dp_debug_obj x)
@@ -58,8 +56,7 @@ let (dp_trace_obj,_) =
declare_object
{(default_object "Dp_trace") with
cache_function = (fun (_,x) -> set_trace x);
- load_function = (fun _ (_,x) -> set_trace x);
- export_function = (fun x -> Some x)}
+ load_function = (fun _ (_,x) -> set_trace x)}
let dp_trace x = Lib.add_anonymous_leaf (dp_trace_obj x)
@@ -818,8 +815,7 @@ let (dp_prelude_obj,_) =
declare_object
{(default_object "Dp_prelude") with
cache_function = (fun (_,x) -> set_prelude x);
- load_function = (fun _ (_,x) -> set_prelude x);
- export_function = (fun x -> Some x)}
+ load_function = (fun _ (_,x) -> set_prelude x)}
let dp_prelude x = Lib.add_anonymous_leaf (dp_prelude_obj x)
@@ -1061,8 +1057,7 @@ let (dp_hint_obj,_) =
declare_object
{(default_object "Dp_hint") with
cache_function = (fun (_,l) -> dp_hint l);
- load_function = (fun _ (_,l) -> dp_hint l);
- export_function = (fun x -> Some x)}
+ load_function = (fun _ (_,l) -> dp_hint l)}
let dp_hint l = Lib.add_anonymous_leaf (dp_hint_obj l)
@@ -1088,8 +1083,7 @@ let (dp_predefined_obj,_) =
declare_object
{(default_object "Dp_predefined") with
cache_function = (fun (_,(id,s)) -> dp_predefined id s);
- load_function = (fun _ (_,(id,s)) -> dp_predefined id s);
- export_function = (fun x -> Some x)}
+ load_function = (fun _ (_,(id,s)) -> dp_predefined id s)}
let dp_predefined id s = Lib.add_anonymous_leaf (dp_predefined_obj (id,s))
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 7a265b526f..9451188aaf 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -415,8 +415,7 @@ let (extr_lang,_) =
declare_object
{(default_object "Extraction Lang") with
cache_function = (fun (_,l) -> lang_ref := l);
- load_function = (fun _ (_,l) -> lang_ref := l);
- export_function = (fun x -> Some x)}
+ load_function = (fun _ (_,l) -> lang_ref := l)}
let _ = declare_summary "Extraction Lang"
{ freeze_function = (fun () -> !lang_ref);
@@ -449,7 +448,6 @@ let (inline_extraction,_) =
{(default_object "Extraction Inline") with
cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
- export_function = (fun x -> Some x);
classify_function = (fun o -> Substitute o);
subst_function =
(fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
@@ -492,8 +490,7 @@ let (reset_inline,_) =
declare_object
{(default_object "Reset Extraction Inline") with
cache_function = (fun (_,_)-> inline_table := empty_inline_table);
- load_function = (fun _ (_,_)-> inline_table := empty_inline_table);
- export_function = (fun x -> Some x)}
+ load_function = (fun _ (_,_)-> inline_table := empty_inline_table)}
let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
@@ -530,7 +527,6 @@ let (blacklist_extraction,_) =
{(default_object "Extraction Blacklist") with
cache_function = (fun (_,l) -> add_blacklist_entries l);
load_function = (fun _ (_,l) -> add_blacklist_entries l);
- export_function = (fun x -> Some x);
classify_function = (fun o -> Libobject.Keep o);
subst_function = (fun (_,_,x) -> x)
}
@@ -558,8 +554,7 @@ let (reset_blacklist,_) =
declare_object
{(default_object "Reset Extraction Blacklist") with
cache_function = (fun (_,_)-> blacklist_table := Idset.empty);
- load_function = (fun _ (_,_)-> blacklist_table := Idset.empty);
- export_function = (fun x -> Some x)}
+ load_function = (fun _ (_,_)-> blacklist_table := Idset.empty)}
let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ())
@@ -588,7 +583,6 @@ let (in_customs,_) =
{(default_object "ML extractions") with
cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
load_function = (fun _ (_,(r,ids,s)) -> add_custom r ids s);
- export_function = (fun x -> Some x);
classify_function = (fun o -> Substitute o);
subst_function =
(fun (_,s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4
index 2b4651dfb9..7ac5f4e89e 100644
--- a/plugins/field/field.ml4
+++ b/plugins/field/field.ml4
@@ -65,7 +65,6 @@ let subst_addfield (_,subst,(typ,th as obj)) =
let th' = subst_mps subst th in
if typ' == typ && th' == th then obj else
(typ',th')
-let export_addfield x = Some x
(* Declaration of the Add Field library object *)
let (in_addfield,out_addfield)=
@@ -73,8 +72,7 @@ let (in_addfield,out_addfield)=
Libobject.open_function = (fun i o -> if i=1 then cache_addfield o);
Libobject.cache_function = cache_addfield;
Libobject.subst_function = subst_addfield;
- Libobject.classify_function = (fun a -> Libobject.Substitute a);
- Libobject.export_function = export_addfield }
+ Libobject.classify_function = (fun a -> Libobject.Substitute a)}
(* Adds a theory to the table *)
let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 06f3291fe6..600a9123b4 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -352,8 +352,6 @@ let subst_Function (_,subst,finfos) =
let classify_Function infos = Libobject.Substitute infos
-let export_Function infos = Some infos
-
let discharge_Function (_,finfos) =
let function_constant' = Lib.discharge_con finfos.function_constant
@@ -410,7 +408,6 @@ let in_Function,out_Function =
Libobject.load_function = load_Function;
Libobject.classify_function = classify_Function;
Libobject.subst_function = subst_Function;
- Libobject.export_function = export_Function;
Libobject.discharge_function = discharge_Function
(* Libobject.open_function = open_Function; *)
}
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index bf3b8ef6f8..6ee12ebcb3 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -265,15 +265,13 @@ let subst_th (_,subst,(c,th as obj)) =
(c',th')
-let (theory_to_obj, obj_to_theory) =
- let cache_th (_,(c, th)) = theories_map_add (c,th)
- and export_th x = Some x in
+let (theory_to_obj, obj_to_theory) =
+ 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);
cache_function = cache_th;
subst_function = subst_th;
- classify_function = (fun x -> Substitute x);
- export_function = export_th }
+ classify_function = (fun x -> Substitute x) }
(* from the set A, guess the associated theory *)
(* With this simple solution, the theory to use is automatically guessed *)
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index c6d9bf44a0..a930fee17b 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -440,16 +440,14 @@ let subst_th (_,subst,th) =
ring_post_tac = posttac' }
-let (theory_to_obj, obj_to_theory) =
- let cache_th (name,th) = add_entry name th
- and export_th x = Some x in
+let (theory_to_obj, obj_to_theory) =
+ let cache_th (name,th) = add_entry name th in
declare_object
{(default_object "tactic-new-ring-theory") with
open_function = (fun i o -> if i=1 then cache_th o);
cache_function = cache_th;
subst_function = subst_th;
- classify_function = (fun x -> Substitute x);
- export_function = export_th }
+ classify_function = (fun x -> Substitute x)}
let setoid_of_relation env a r =
@@ -1018,16 +1016,14 @@ let subst_th (_,subst,th) =
field_pre_tac = pretac';
field_post_tac = posttac' }
-let (ftheory_to_obj, obj_to_ftheory) =
- let cache_th (name,th) = add_field_entry name th
- and export_th x = Some x in
+let (ftheory_to_obj, obj_to_ftheory) =
+ let cache_th (name,th) = add_field_entry name th in
declare_object
{(default_object "tactic-new-field-theory") with
open_function = (fun i o -> if i=1 then cache_th o);
cache_function = cache_th;
subst_function = subst_th;
- classify_function = (fun x -> Substitute x);
- export_function = export_th }
+ classify_function = (fun x -> Substitute x) }
let field_equality r inv req =
match kind_of_term req with
diff --git a/plugins/subtac/subtac_obligations.ml b/plugins/subtac/subtac_obligations.ml
index 94bd059c2d..76a8a03221 100644
--- a/plugins/subtac/subtac_obligations.ml
+++ b/plugins/subtac/subtac_obligations.ml
@@ -170,8 +170,7 @@ let (input,output) =
prlist_with_sep spc (fun x -> Nameops.pr_id x)
(map_keys infos));
Substitute (ProgMap.empty, tac));
- subst_function = subst;
- export_function = (fun x -> Some x) }
+ subst_function = subst}
let update_state () =
(* msgnl (str "Updating obligations info"); *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:29:29 +0000