Stylistic improvements in intf/decl_kinds.mli.

We get rid of tuples containing booleans (typically for universe
polymorphism) by replacing them with records.

The previously common idom:

if pi2 kind (* polymorphic *) then ... else ...

becomes:

if kind.polymorphic then ... else ...

To make the construction and destruction of these records lightweight,
the labels of boolean arguments for universe polymorphism are now
usually also called "polymorphic".

1 files changed, 4 insertions, 3 deletions

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index a45effb16..8c6673732 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