From db22177ab61bf516a75bb160d79efbfb97c3c38d Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 29 Aug 2019 15:35:19 +0200
Subject: [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.
---
 plugins/funind/indfun_common.mli | 9 ---------
 1 file changed, 9 deletions(-)

(limited to 'plugins/funind/indfun_common.mli')

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
-- 
cgit v1.2.3