Merge remote-tracking branch 'github/pr/283' into trunk

Was PR#283: Stylistic improvements in intf/decl_kinds.mli.

1 files changed, 4 insertions, 3 deletions

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index a45effb167..8c66737324 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -148,17 +148,18 @@ let get_locality = function
 | Local -> true
 | Global -> false
 
-let save with_clean id const (locality,_,kind) hook =
+let save with_clean id const goal_kind hook =
   let fix_exn = Future.fix_exn_of const.const_entry_body in
+  let locality = goal_kind.locality in
   let l,r = match locality with
     | Discharge when Lib.sections_are_opened () ->
-        let k = Kindops.logical_kind_of_goal_kind kind in
+        let k = Kindops.logical_kind_of_goal_kind goal_kind.object_kind in
 	let c = SectionLocalDef const in
 	let _ = declare_variable id (Lib.cwd(), c, k) in
 	(Local, VarRef id)
     | Discharge | Local | Global ->
         let local = get_locality locality in
-        let k = Kindops.logical_kind_of_goal_kind kind in
+        let k = Kindops.logical_kind_of_goal_kind goal_kind.object_kind in
         let kn = declare_constant id ~local (DefinitionEntry const, k) in
 	(locality, ConstRef kn)
   in