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 /plugins/ltac | |
| parent | 4ecbad30c77316294c8625ead722d469c1c7f79d (diff) | |
| parent | 264c208a5eb824c880ef4c46e060185470064df5 (diff) | |
Merge PR #8096: Higher-level libobject API for objects with fixed scopes
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/extratactics.mlg | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index ec2adf065a..47f593ff3e 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -531,11 +531,9 @@ let cache_transitivity_lemma (_,(left,lem)) = let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref) let inTransitivity : bool * Constr.t -> obj = - declare_object {(default_object "TRANSITIVITY-STEPS") with - cache_function = cache_transitivity_lemma; - open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o); - subst_function = subst_transitivity_lemma; - classify_function = (fun o -> Substitute o) } + declare_object @@ global_object_nodischarge "TRANSITIVITY-STEPS" + ~cache:cache_transitivity_lemma + ~subst:(Some subst_transitivity_lemma) (* Main entry points *) |