diff options
| author | Maxime Dénès | 2018-07-19 11:41:48 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-12-12 18:41:11 +0100 |
| commit | 264c208a5eb824c880ef4c46e060185470064df5 (patch) | |
| tree | ce99aabb06f6232d4ecfd2117269d827df24463c /tactics | |
| parent | dfd4c4a2b50edf894a19cd50c43517e1804eadc9 (diff) | |
Higher-level libobject API for objects with fixed scopes
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/autorewrite.ml | 13 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 10 |
2 files changed, 8 insertions, 15 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 76cbdee0d5..f824552705 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -196,17 +196,12 @@ let subst_hintrewrite (subst,(rbase,list as node)) = if list' == list then node else (rbase,list') -let classify_hintrewrite x = Libobject.Substitute x - - (* Declaration of the Hint Rewrite library object *) let inHintRewrite : string * HintDN.t -> Libobject.obj = - Libobject.declare_object {(Libobject.default_object "HINT_REWRITE") with - Libobject.cache_function = cache_hintrewrite; - Libobject.load_function = (fun _ -> cache_hintrewrite); - Libobject.subst_function = subst_hintrewrite; - Libobject.classify_function = classify_hintrewrite } - + let open Libobject in + declare_object @@ superglobal_object_nodischarge "HINT_REWRITE" + ~cache:cache_hintrewrite + ~subst:(Some subst_hintrewrite) open Clenv diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index a53e3bf20d..a67f5f6d6e 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -59,12 +59,10 @@ let discharge_scheme (_,(kind,l)) = Some (kind, l) let inScheme : string * (inductive * Constant.t) array -> obj = - declare_object {(default_object "SCHEME") with - cache_function = cache_scheme; - load_function = (fun _ -> cache_scheme); - subst_function = subst_scheme; - classify_function = (fun obj -> Substitute obj); - discharge_function = discharge_scheme} + declare_object @@ superglobal_object "SCHEME" + ~cache:cache_scheme + ~subst:(Some subst_scheme) + ~discharge:discharge_scheme (**********************************************************************) (* The table of scheme building functions *) |