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".

7 files changed, 61 insertions, 45 deletions

diff --git a/library/declare.ml b/library/declare.ml
index cc8415cf47..36a58629e6 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -44,7 +44,9 @@ let if_xml f x = if !Flags.xml_export then f x else ()
 
 type section_variable_entry =
   | SectionLocalDef of Safe_typing.private_constants definition_entry
-  | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
+  | SectionLocalAssum of { type_context : types Univ.in_universe_context_set;
+                           polymorphic : bool;
+                           binding_kind : binding_kind }
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
 
@@ -56,19 +58,22 @@ let cache_variable ((sp,_),o) =
   if variable_exists id then
     alreadydeclared (pr_id id ++ str " already exists");
 
-  let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
-    | SectionLocalAssum ((ty,ctx),poly,impl) ->
-      let () = Global.push_named_assum ((id,ty,poly),ctx) in
-      let impl = if impl then Implicit else Explicit in
-	impl, true, poly, ctx
+  let impl,opaque,polymorphic,ctx = match d with (* Fails if not well-typed *)
+    | SectionLocalAssum { type_context = (ty,ctx); polymorphic; binding_kind } ->
+      let () = Global.push_named_assum ((id,ty,polymorphic),ctx) in
+	binding_kind, true, polymorphic, ctx
     | SectionLocalDef (de) ->
       let univs = Global.push_named_def (id,de) in
       Explicit, de.const_entry_opaque,
       de.const_entry_polymorphic, univs in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
-  add_section_variable id impl poly ctx;
+  add_section_variable id impl ~polymorphic ctx;
   Dischargedhypsmap.set_discharged_hyps sp [];
-  add_variable_data id (p,opaq,ctx,poly,mk)
+  add_variable_data id { dir_path = p;
+                         opaque;
+                         universe_context_set = ctx;
+                         polymorphic;
+                         kind = mk }
 
 let discharge_variable (_,o) = match o with
   | Inr (id,_) ->
@@ -236,11 +241,11 @@ let declare_constant_common id cst =
   c
 
 let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
-    ?(poly=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body =
+    ?(polymorphic=false) ?(univs=Univ.UContext.empty) ?(eff=Safe_typing.empty_private_constants) body =
   { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
     const_entry_secctx = None;
     const_entry_type = types;
-    const_entry_polymorphic = poly;
+    const_entry_polymorphic = polymorphic;
     const_entry_universes = univs;
     const_entry_opaque = opaque;
     const_entry_feedback = None;
@@ -272,9 +277,9 @@ let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(e
 
 let declare_definition ?(internal=UserIndividualRequest)
   ?(opaque=false) ?(kind=Decl_kinds.Definition) ?(local = false)
-  ?(poly=false) id ?types (body,ctx) =
+  ?(polymorphic=false) id ?types (body,ctx) =
   let cb =
-    definition_entry ?types ~poly ~univs:(Univ.ContextSet.to_context ctx) ~opaque body
+    definition_entry ?types ~polymorphic ~univs:(Univ.ContextSet.to_context ctx) ~opaque body
   in
     declare_constant ~internal ~local id
       (Entries.DefinitionEntry cb, Decl_kinds.IsDefinition kind)
@@ -458,10 +463,10 @@ let input_universes : universe_decl -> Libobject.obj =
       discharge_function = (fun (_, (p, _ as x)) -> if p then None else Some x);
       classify_function = (fun a -> Keep a) }
 
-let do_universe poly l =
+let do_universe ~polymorphic l =
   let in_section = Lib.sections_are_opened () in
   let () =
-    if poly && not in_section then
+    if polymorphic && not in_section then
       user_err ~hdr:"Constraint"
                    (str"Cannot declare polymorphic universes outside sections")
   in
@@ -470,7 +475,7 @@ let do_universe poly l =
 	      let lev = Universes.new_univ_level (Global.current_dirpath ()) in
 	      (id, lev)) l
   in
-    Lib.add_anonymous_leaf (input_universes (poly, l))
+    Lib.add_anonymous_leaf (input_universes (polymorphic, l))
 
 type constraint_decl = polymorphic * Univ.constraints
 
@@ -490,7 +495,7 @@ let input_constraints : constraint_decl -> Libobject.obj =
       discharge_function = discharge_constraints;
       classify_function = (fun a -> Keep a) }
 
-let do_constraint poly l =
+let do_constraint ~polymorphic l =
   let u_of_id =
     let names, _ = Universes.global_universe_names () in
     fun (loc, id) ->
@@ -500,12 +505,12 @@ let do_constraint poly l =
   in
   let in_section = Lib.sections_are_opened () in
   let () =
-    if poly && not in_section then
+    if polymorphic && not in_section then
       user_err ~hdr:"Constraint"
                     (str"Cannot declare polymorphic constraints outside sections")
   in
   let check_poly loc p loc' p' =
-    if poly then ()
+    if polymorphic then ()
     else if p || p' then
       let loc = if p then loc else loc' in
       user_err ~loc ~hdr:"Constraint"
@@ -519,4 +524,4 @@ let do_constraint poly l =
      Univ.Constraint.add (lu, d, ru) acc)
     Univ.Constraint.empty l
   in
-    Lib.add_anonymous_leaf (input_constraints (poly, constraints))
+    Lib.add_anonymous_leaf (input_constraints (polymorphic, constraints))
diff --git a/library/declare.mli b/library/declare.mli
index 7824506da0..760bf437b7 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -23,7 +23,9 @@ open Decl_kinds
 
 type section_variable_entry =
   | SectionLocalDef of Safe_typing.private_constants definition_entry
-  | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
+  | SectionLocalAssum of { type_context : types Univ.in_universe_context_set;
+                           polymorphic : bool;
+                           binding_kind : binding_kind }
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
 
@@ -42,7 +44,7 @@ type internal_flag =
 (* Defaut definition entries, transparent with no secctx or proj information *)
 val definition_entry : ?fix_exn:Future.fix_exn ->
   ?opaque:bool -> ?inline:bool -> ?types:types ->
-  ?poly:polymorphic -> ?univs:Univ.universe_context ->
+  ?polymorphic:bool -> ?univs:Univ.universe_context ->
   ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
 
 (** [declare_constant id cd] declares a global declaration
@@ -56,7 +58,7 @@ val declare_constant :
 
 val declare_definition : 
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
-  ?local:bool -> ?poly:polymorphic -> Id.t -> ?types:constr -> 
+  ?local:bool -> ?polymorphic:bool -> Id.t -> ?types:constr -> 
   constr Univ.in_universe_context_set -> constant
 
 (** Since transparent constants' side effects are globally declared, we
@@ -89,5 +91,6 @@ val exists_name : Id.t -> bool
 
 (** Global universe names and constraints *)
 
-val do_universe : polymorphic -> Id.t Loc.located list -> unit
-val do_constraint : polymorphic -> (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit
+val do_universe : polymorphic:bool -> Id.t Loc.located list -> unit
+val do_constraint : polymorphic:bool ->
+  (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit
diff --git a/library/decls.ml b/library/decls.ml
index 2952c258a5..1e9afe9687 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -19,18 +19,22 @@ module NamedDecl = Context.Named.Declaration
 (** Datas associated to section variables and local definitions *)
 
 type variable_data =
-  DirPath.t * bool (* opacity *) * Univ.universe_context_set * polymorphic * logical_kind
+  { dir_path : DirPath.t;
+    opaque : bool;
+    universe_context_set : Univ.universe_context_set;
+    polymorphic : bool;
+    kind : logical_kind }
 
 let vartab =
   Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE"
 
 let add_variable_data id o = vartab := Id.Map.add id o !vartab
 
-let variable_path id = let (p,_,_,_,_) = Id.Map.find id !vartab in p
-let variable_opacity id = let (_,opaq,_,_,_) = Id.Map.find id !vartab in opaq
-let variable_kind id = let (_,_,_,_,k) = Id.Map.find id !vartab in k
-let variable_context id = let (_,_,ctx,_,_) = Id.Map.find id !vartab in ctx
-let variable_polymorphic id = let (_,_,_,p,_) = Id.Map.find id !vartab in p
+let variable_path id = (Id.Map.find id !vartab).dir_path
+let variable_opacity id = (Id.Map.find id !vartab).opaque
+let variable_kind id = (Id.Map.find id !vartab).kind
+let variable_context id = (Id.Map.find id !vartab).universe_context_set
+let variable_polymorphic id = (Id.Map.find id !vartab).polymorphic
 
 let variable_secpath id =
   let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in
diff --git a/library/decls.mli b/library/decls.mli
index 1ca7f89469..e84a6376b9 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -17,7 +17,11 @@ open Decl_kinds
 (** Registration and access to the table of variable *)
 
 type variable_data =
-  DirPath.t * bool (** opacity *) * Univ.universe_context_set * polymorphic * logical_kind
+  { dir_path : DirPath.t;
+    opaque : bool;
+    universe_context_set : Univ.universe_context_set;
+    polymorphic : bool;
+    kind : logical_kind }
 
 val add_variable_data : variable -> variable_data -> unit
 val variable_path : variable -> DirPath.t
diff --git a/library/kindops.ml b/library/kindops.ml
index 21b1bec33c..3d737e5acc 100644
--- a/library/kindops.ml
+++ b/library/kindops.ml
@@ -24,9 +24,9 @@ let string_of_theorem_kind = function
   | Corollary -> "Corollary"
 
 let string_of_definition_kind def =
-  let (locality, poly, kind) = def in
+  let locality = def.locality in
   let error () = CErrors.anomaly (Pp.str "Internal definition kind") in
-  match kind with
+  match def.object_kind with
   | Definition ->
     begin match locality with
     | Discharge -> "Let"
diff --git a/library/lib.ml b/library/lib.ml
index 749cc4ff3e..954889fb6b 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -416,12 +416,12 @@ let check_same_poly p vars =
   if List.exists pred vars then
     error "Cannot mix universe polymorphic and monomorphic declarations in sections."
 
-let add_section_variable id impl poly ctx =
+let add_section_variable id impl ~polymorphic ctx =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | (vars,repl,abs)::sl ->
-       List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab;
-       sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl
+       List.iter (fun tab -> check_same_poly polymorphic (pi1 tab)) !sectab;
+       sectab := (Variable (id,impl,polymorphic,ctx)::vars,repl,abs)::sl
 
 let add_section_context ctx =
   match !sectab with
@@ -450,11 +450,11 @@ let instance_from_variable_context =
 let named_of_variable_context =
   List.map fst
   
-let add_section_replacement f g poly hyps =
+let add_section_replacement f g ~polymorphic hyps =
   match !sectab with
   | [] -> ()
   | (vars,exps,abs)::sl ->
-    let () = check_same_poly poly vars in
+    let () = check_same_poly polymorphic vars in
     let sechyps,ctx = extract_hyps (vars,hyps) in
     let ctx = Univ.ContextSet.to_context ctx in
     let subst, ctx = Univ.abstract_universes true ctx in
@@ -462,13 +462,13 @@ let add_section_replacement f g poly hyps =
     sectab := (vars,f (Univ.UContext.instance ctx,args) exps,
 	      g (sechyps,subst,ctx) abs)::sl
 
-let add_section_kn poly kn =
+let add_section_kn ~polymorphic kn =
   let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
-    add_section_replacement f f poly
+    add_section_replacement f f ~polymorphic
 
-let add_section_constant poly kn =
+let add_section_constant ~polymorphic kn =
   let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
-    add_section_replacement f f poly
+    add_section_replacement f f ~polymorphic
 
 let replacement_context () = pi2 (List.hd !sectab)
 
diff --git a/library/lib.mli b/library/lib.mli
index 092643c2d8..e905ee57e2 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -176,11 +176,11 @@ val variable_section_segment_of_reference : Globnames.global_reference -> variab
 val section_instance : Globnames.global_reference -> Univ.universe_instance * Names.Id.t array
 val is_in_section : Globnames.global_reference -> bool
 
-val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.universe_context_set -> unit
+val add_section_variable : Names.Id.t -> Decl_kinds.binding_kind -> polymorphic:bool -> Univ.universe_context_set -> unit
 val add_section_context : Univ.universe_context_set -> unit
-val add_section_constant : Decl_kinds.polymorphic ->
+val add_section_constant : polymorphic:bool ->
   Names.constant -> Context.Named.t -> unit
-val add_section_kn : Decl_kinds.polymorphic ->
+val add_section_kn : polymorphic:bool ->
   Names.mutual_inductive -> Context.Named.t -> unit
 val replacement_context : unit -> Opaqueproof.work_list