[api] Remove `polymorphic` type alias, use labels instead.

This is more in-line with attributes and the rest of the API, and
makes some code significantly clearer (as in `foo true false false`,
etc...)

5 files changed, 12 insertions, 16 deletions

diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 57612c3735..2735a9118e 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -14,8 +14,6 @@ type discharge = DoDischarge | NoDischarge
 
 type binding_kind = Explicit | Implicit
 
-type polymorphic = bool
-
 type private_flag = bool
 
 type cumulative_inductive_flag = bool
diff --git a/library/decls.ml b/library/decls.ml
index ef60a44ac7..104eb37011 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -18,7 +18,7 @@ open Libnames
 (** Datas associated to section variables and local definitions *)
 
 type variable_data =
-  DirPath.t * bool (* opacity *) * Univ.ContextSet.t * polymorphic * logical_kind
+  DirPath.t * bool (* opacity *) * Univ.ContextSet.t * bool (* poly *) * logical_kind
 
 let vartab =
   Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE"
diff --git a/library/decls.mli b/library/decls.mli
index 0d09499b51..93298c0bc4 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -19,7 +19,7 @@ open Decl_kinds
 (** Registration and access to the table of variable *)
 
 type variable_data =
-  DirPath.t * bool (* opacity *) * Univ.ContextSet.t * polymorphic * logical_kind
+  DirPath.t * bool (* opacity *) * Univ.ContextSet.t * bool (* poly *) * logical_kind
 
 val add_variable_data : variable -> variable_data -> unit
 val variable_path : variable -> DirPath.t
@@ -27,7 +27,7 @@ val variable_secpath : variable -> qualid
 val variable_kind : variable -> logical_kind
 val variable_opacity : variable -> bool
 val variable_context : variable -> Univ.ContextSet.t
-val variable_polymorphic : variable -> polymorphic
+val variable_polymorphic : variable -> bool
 val variable_exists : variable -> bool
 
 (** Registration and access to the table of constants *)
diff --git a/library/lib.ml b/library/lib.ml
index ae657dbd70..e4054d58cc 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -411,8 +411,8 @@ type abstr_info = {
 type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
 
 type secentry =
-  | Variable of (Names.Id.t * Decl_kinds.binding_kind *
-		   Decl_kinds.polymorphic * Univ.ContextSet.t)
+  | Variable of (Names.Id.t * Decl_kinds.binding_kind * bool * Univ.ContextSet.t)
+  (** (name, kind, poly, univs) *)
   | Context of Univ.ContextSet.t
 
 let sectab =
@@ -428,12 +428,12 @@ let check_same_poly p vars =
   if List.exists pred vars then
     user_err Pp.(str  "Cannot mix universe polymorphic and monomorphic declarations in sections.")
 
-let add_section_variable id impl poly ctx =
+let add_section_variable ~name ~kind ~poly 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
+       sectab := (Variable (name,kind,poly,ctx)::vars,repl,abs)::sl
 
 let add_section_context ctx =
   match !sectab with
@@ -509,11 +509,11 @@ let add_section_replacement f g poly hyps =
     } in
     sectab := (vars,f (inst,args) exps, g info abs) :: sl
 
-let add_section_kn poly kn =
+let add_section_kn ~poly kn =
   let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
     add_section_replacement f f poly
 
-let add_section_constant poly kn =
+let add_section_constant ~poly kn =
   let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
     add_section_replacement f f poly
 
diff --git a/library/lib.mli b/library/lib.mli
index f6bd61e2da..2cd43b66b3 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -178,12 +178,10 @@ val variable_section_segment_of_reference : GlobRef.t -> variable_context
 val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array
 val is_in_section : GlobRef.t -> bool
 
-val add_section_variable : Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit
+val add_section_variable : name:Id.t -> kind:Decl_kinds.binding_kind -> poly:bool -> Univ.ContextSet.t -> unit
 val add_section_context : Univ.ContextSet.t -> unit
-val add_section_constant : Decl_kinds.polymorphic ->
-  Constant.t -> Constr.named_context -> unit
-val add_section_kn : Decl_kinds.polymorphic ->
-  MutInd.t -> Constr.named_context -> unit
+val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit
+val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit
 val replacement_context : unit -> Opaqueproof.work_list
 
 val is_polymorphic_univ : Univ.Level.t -> bool