From d31056ec924ef6e09b28bc3822b427b67a8a300b Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 12 Feb 2019 22:37:33 +0100
Subject: [vernac] Unify declaration hooks.

Supersedes #8718.
---
 plugins/funind/indfun_common.mli | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

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

diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 9584649cff..1e0b95df34 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -42,7 +42,14 @@ val const_of_id: Id.t ->  GlobRef.t(* constantyes *)
 val jmeq : unit -> EConstr.constr
 val jmeq_refl : unit -> EConstr.constr
 
-val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> ?hook:Lemmas.declaration_hook -> Decl_kinds.goal_kind -> unit
+val save
+  :  bool
+  -> Id.t
+  -> Safe_typing.private_constants Entries.definition_entry
+  -> ?hook:Lemmas.declaration_hook
+  -> UState.t
+  -> Decl_kinds.goal_kind
+  -> unit
 
 (* [with_full_print f a] applies [f] to [a] in full printing environment.
 
-- 
cgit v1.2.3