diff options
| author | Enrico Tassi | 2018-12-13 09:27:39 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2018-12-13 09:27:39 +0100 |
| commit | d9a6d4814f0669b586ca5c13d6d6540cd194b45f (patch) | |
| tree | f0f8582ff2c85eee0e7b42e253ad8358912c7f12 /tactics | |
| parent | 4ecbad30c77316294c8625ead722d469c1c7f79d (diff) | |
| parent | 264c208a5eb824c880ef4c46e060185470064df5 (diff) | |
Merge PR #8096: 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 *) |