diff options
| author | Emilio Jesus Gallego Arias | 2019-08-29 15:35:19 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-08-29 17:17:57 +0200 |
| commit | db22177ab61bf516a75bb160d79efbfb97c3c38d (patch) | |
| tree | 7b51e86866de46b8d7a5e58ac07921bb535d232e /plugins/funind/indfun_common.mli | |
| parent | 7153cc3a4d886944f9e09a10ea106cefb1e9d0f8 (diff) | |
[funind] Don't export duplicate save function.
It will take a bit more to clean up the mess with entries in the
`indfun` plugin [quite a few PRs in the queue], but thanks to recent
refactoring the tricky parts are self-contained now in `gen_principle`
so we can remove the duplicated `save` function from the public API.
Diffstat (limited to 'plugins/funind/indfun_common.mli')
| -rw-r--r-- | plugins/funind/indfun_common.mli | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 34fb10bb67..cd5202a6c7 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -42,15 +42,6 @@ val jmeq : unit -> EConstr.constr val jmeq_refl : unit -> EConstr.constr val make_eq : unit -> EConstr.constr -val save - : Id.t - -> Evd.side_effects Declare.proof_entry - -> ?hook:DeclareDef.Hook.t - -> UState.t - -> DeclareDef.locality - -> Decls.logical_kind - -> unit - (* [with_full_print f a] applies [f] to [a] in full printing environment. This function preserves the print settings |