[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...)

13 files changed, 94 insertions, 85 deletions

diff --git a/vernac/class.ml b/vernac/class.ml
index 9c22d24f93..febe8e34e4 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -338,21 +338,21 @@ let try_add_new_coercion_core ref ~local c d e f =
       user_err ~hdr:"try_add_new_coercion_core"
         (explain_coercion_error ref e ++ str ".")
 
-let try_add_new_coercion ref ~local poly =
+let try_add_new_coercion ref ~local ~poly =
   try_add_new_coercion_core ref ~local poly None None false
 
-let try_add_new_coercion_subclass cl ~local poly =
+let try_add_new_coercion_subclass cl ~local ~poly =
   let coe_ref = build_id_coercion None cl poly in
   try_add_new_coercion_core coe_ref ~local poly (Some cl) None true
 
-let try_add_new_coercion_with_target ref ~local poly ~source ~target =
+let try_add_new_coercion_with_target ref ~local ~poly ~source ~target =
   try_add_new_coercion_core ref ~local poly (Some source) (Some target) false
 
-let try_add_new_identity_coercion id ~local poly ~source ~target =
+let try_add_new_identity_coercion id ~local ~poly ~source ~target =
   let ref = build_id_coercion (Some id) source poly in
   try_add_new_coercion_core ref ~local poly (Some source) (Some target) true
 
-let try_add_new_coercion_with_source ref ~local poly ~source =
+let try_add_new_coercion_with_source ref ~local ~poly ~source =
   try_add_new_coercion_core ref ~local poly (Some source) None false
 
 let add_coercion_hook poly _uctx _trans local ref =
@@ -362,13 +362,13 @@ let add_coercion_hook poly _uctx _trans local ref =
   | Global ImportNeedQualified -> true
   | Global ImportDefaultBehavior -> false
   in
-  let () = try_add_new_coercion ref ~local poly in
+  let () = try_add_new_coercion ref ~local ~poly in
   let msg = Nametab.pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
   Flags.if_verbose Feedback.msg_info msg
 
-let add_coercion_hook poly = DeclareDef.Hook.make (add_coercion_hook poly)
+let add_coercion_hook ~poly = DeclareDef.Hook.make (add_coercion_hook poly)
 
-let add_subclass_hook poly _uctx _trans local ref =
+let add_subclass_hook ~poly _uctx _trans local ref =
   let open DeclareDef in
   let stre = match local with
   | Discharge -> assert false (* Local Subclass in section behaves like Local Definition *)
@@ -376,6 +376,6 @@ let add_subclass_hook poly _uctx _trans local ref =
   | Global ImportDefaultBehavior -> false
   in
   let cl = class_of_global ref in
-  try_add_new_coercion_subclass cl ~local:stre poly
+  try_add_new_coercion_subclass cl ~local:stre ~poly
 
-let add_subclass_hook poly = DeclareDef.Hook.make (add_subclass_hook poly)
+let add_subclass_hook ~poly = DeclareDef.Hook.make (add_subclass_hook ~poly)
diff --git a/vernac/class.mli b/vernac/class.mli
index d530d218d4..3254d5d981 100644
--- a/vernac/class.mli
+++ b/vernac/class.mli
@@ -15,35 +15,39 @@ open Classops
 
 (** [try_add_new_coercion_with_target ref s src tg] declares [ref] as a coercion
    from [src] to [tg] *)
-val try_add_new_coercion_with_target : GlobRef.t -> local:bool ->
-  Decl_kinds.polymorphic ->
-  source:cl_typ -> target:cl_typ ->  unit
+val try_add_new_coercion_with_target
+  :  GlobRef.t
+  -> local:bool
+  -> poly:bool
+  -> source:cl_typ
+  -> target:cl_typ
+  -> unit
 
 (** [try_add_new_coercion ref s] declares [ref], assumed to be of type
    [(x1:T1)...(xn:Tn)src->tg], as a coercion from [src] to [tg] *)
-val try_add_new_coercion : GlobRef.t -> local:bool ->
-  Decl_kinds.polymorphic -> unit
+val try_add_new_coercion : GlobRef.t -> local:bool -> poly:bool -> unit
 
 (** [try_add_new_coercion_subclass cst s] expects that [cst] denotes a
    transparent constant which unfolds to some class [tg]; it declares
    an identity coercion from [cst] to [tg], named something like
    ["Id_cst_tg"] *)
-val try_add_new_coercion_subclass : cl_typ -> local:bool -> 
-  Decl_kinds.polymorphic -> unit
+val try_add_new_coercion_subclass : cl_typ -> local:bool -> poly:bool -> unit
 
 (** [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion
    from [src] to [tg] where the target is inferred from the type of [ref] *)
 val try_add_new_coercion_with_source : GlobRef.t -> local:bool ->
-  Decl_kinds.polymorphic -> source:cl_typ -> unit
+  poly:bool -> source:cl_typ -> unit
 
 (** [try_add_new_identity_coercion id s src tg] enriches the
    environment with a new definition of name [id] declared as an
    identity coercion from [src] to [tg] *)
-val try_add_new_identity_coercion : Id.t -> local:bool -> 
-  Decl_kinds.polymorphic -> source:cl_typ -> target:cl_typ -> unit
+val try_add_new_identity_coercion
+  :  Id.t
+  -> local:bool
+  -> poly:bool -> source:cl_typ -> target:cl_typ -> unit
 
-val add_coercion_hook : Decl_kinds.polymorphic -> DeclareDef.Hook.t
+val add_coercion_hook : poly:bool -> DeclareDef.Hook.t
 
-val add_subclass_hook : Decl_kinds.polymorphic -> DeclareDef.Hook.t
+val add_subclass_hook : poly:bool -> DeclareDef.Hook.t
 
 val class_of_global : GlobRef.t -> cl_typ
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 98c71689f4..8addfa054e 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -567,7 +567,7 @@ let new_instance_common ~program_mode ~generalize env instid ctx cl =
   id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl
 
 let new_instance_interactive ?(global=false)
-    poly instid ctx cl
+    ~poly instid ctx cl
     ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
   let env = Global.env() in
   let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
@@ -576,7 +576,7 @@ let new_instance_interactive ?(global=false)
     cty k u ctx ctx' pri decl imps subst id
 
 let new_instance_program ?(global=false)
-    poly instid ctx cl opt_props
+    ~poly instid ctx cl opt_props
     ?(generalize=true) ?hook pri =
   let env = Global.env() in
   let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
@@ -586,7 +586,7 @@ let new_instance_program ?(global=false)
   id
 
 let new_instance ?(global=false)
-    poly instid ctx cl props
+    ~poly instid ctx cl props
     ?(generalize=true) ?hook pri =
   let env = Global.env() in
   let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
@@ -595,7 +595,7 @@ let new_instance ?(global=false)
     cty k u ctx ctx' pri decl imps subst id props;
   id
 
-let declare_new_instance ?(global=false) ~program_mode poly instid ctx cl pri =
+let declare_new_instance ?(global=false) ~program_mode ~poly instid ctx cl pri =
   let env = Global.env() in
   let ({CAst.loc;v=instid}, pl) = instid in
   let sigma, k, u, cty, ctx', ctx, imps, subst, decl =
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 472690cdd4..1247fdc8c1 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -27,7 +27,7 @@ val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit
 
 val new_instance_interactive
   :  ?global:bool (** Not global by default. *)
-  -> Decl_kinds.polymorphic
+  -> poly:bool
   -> name_decl
   -> local_binder_expr list
   -> constr_expr
@@ -39,7 +39,7 @@ val new_instance_interactive
 
 val new_instance
   :  ?global:bool (** Not global by default. *)
-  -> Decl_kinds.polymorphic
+  -> poly:bool
   -> name_decl
   -> local_binder_expr list
   -> constr_expr
@@ -51,7 +51,7 @@ val new_instance
 
 val new_instance_program
   : ?global:bool (** Not global by default. *)
-  -> Decl_kinds.polymorphic
+  -> poly:bool
   -> name_decl
   -> local_binder_expr list
   -> constr_expr
@@ -64,7 +64,7 @@ val new_instance_program
 val declare_new_instance
   : ?global:bool (** Not global by default. *)
   -> program_mode:bool
-  -> Decl_kinds.polymorphic
+  -> poly:bool
   -> ident_decl
   -> local_binder_expr list
   -> constr_expr
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index bf43438c1e..c098df9bef 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -59,7 +59,7 @@ match scope with
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let () = Classes.declare_instance env sigma None true r in
-  let () = if is_coe then Class.try_add_new_coercion r ~local:true false in
+  let () = if is_coe then Class.try_add_new_coercion r ~local:true ~poly:false in
   (r,Univ.Instance.empty,true)
 
 | Global local ->
@@ -79,7 +79,7 @@ match scope with
   let sigma = Evd.from_env env in
   let () = if do_instance then Classes.declare_instance env sigma None false gr in
   let local = match local with ImportNeedQualified -> true | ImportDefaultBehavior -> false in
-  let () = if is_coe then Class.try_add_new_coercion gr ~local poly in
+  let () = if is_coe then Class.try_add_new_coercion gr ~local ~poly in
   let inst = match ctx with
     | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx
     | Monomorphic_entry _ -> Univ.Instance.empty
@@ -228,7 +228,7 @@ let named_of_rel_context l =
       l ([], [])
   in ctx
 
-let context poly l =
+let context ~poly l =
   let env = Global.env() in
   let sigma = Evd.from_env env in
   let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in
@@ -253,7 +253,7 @@ let context poly l =
            separately. *)
         begin
           let uctx = Evd.universe_context_set sigma in
-          Declare.declare_universe_context poly uctx;
+          Declare.declare_universe_context ~poly uctx;
           if poly then Polymorphic_entry ([||], Univ.UContext.empty)
           else Monomorphic_entry Univ.ContextSet.empty
         end
@@ -265,7 +265,7 @@ let context poly l =
            to avoid redeclaring them. *)
         begin
           let uctx = Evd.universe_context_set sigma in
-          Declare.declare_universe_context poly uctx;
+          Declare.declare_universe_context ~poly uctx;
           Monomorphic_entry Univ.ContextSet.empty
         end
   in
@@ -298,7 +298,9 @@ let context poly l =
                Declaremods.NoInline (CAst.make id))
       | Some b ->
         let entry = Declare.definition_entry ~univs ~types:t b in
-        let _gr = DeclareDef.declare_definition ~name:id ~scope:DeclareDef.Discharge ~kind:Definition UnivNames.empty_binders entry [] in
+        let _gr = DeclareDef.declare_definition
+            ~name:id ~scope:DeclareDef.Discharge
+            ~kind:Definition UnivNames.empty_binders entry [] in
         Lib.sections_are_opened () || Lib.is_modtype_strict ()
       in
         status && nstatus
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 4171c99836..0a4130ee13 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -17,7 +17,7 @@ open Decl_kinds
 
 val do_assumptions
   :  program_mode:bool
-  -> poly:polymorphic
+  -> poly:bool
   -> scope:DeclareDef.locality
   -> kind:assumption_object_kind
   -> Declaremods.inline
@@ -44,7 +44,7 @@ val declare_assumption
 (** returns [false] if, for lack of section, it declares an assumption
     (unless in a module type). *)
 val context
-  : Decl_kinds.polymorphic
+  :  poly:bool
   -> local_binder_expr list
   -> bool
 
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 3d5ea319bb..57de719cb4 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -40,7 +40,7 @@ let check_imps ~impsty ~impsbody =
   | [], [] -> () in
   aux impsty impsbody
 
-let interp_definition ~program_mode pl bl poly red_option c ctypopt =
+let interp_definition ~program_mode pl bl ~poly red_option c ctypopt =
   let env = Global.env() in
   (* Explicitly bound universes and constraints *)
   let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in
@@ -81,7 +81,7 @@ let check_definition ~program_mode (ce, evd, _, imps) =
 
 let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_option c ctypopt =
   let (ce, evd, univdecl, imps as def) =
-    interp_definition ~program_mode univdecl bl poly red_option c ctypopt
+    interp_definition ~program_mode univdecl bl ~poly red_option c ctypopt
   in
   if program_mode then
     let env = Global.env () in
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 1058945668..71926a9d23 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -38,7 +38,7 @@ val interp_definition
   :  program_mode:bool
   -> universe_decl_expr option
   -> local_binder_expr list
-  -> polymorphic
+  -> poly:bool
   -> red_expr option
   -> constr_expr
   -> constr_expr option
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 363ba5beff..f530dad4fd 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -349,7 +349,7 @@ let restrict_inductive_universes sigma ctx_params arities constructors =
   let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
   Evd.restrict_universe_context sigma uvars
 
-let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations cum poly prv finite =
+let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations cum ~poly prv finite =
   check_all_names_different indl;
   List.iter check_param paramsl;
   if not (List.is_empty uparamsl) && not (List.is_empty notations)
@@ -469,8 +469,8 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
       InferCumulativity.infer_inductive env_ar mind_ent
    else mind_ent), Evd.universe_binders sigma, impls
 
-let interp_mutual_inductive ~template udecl (paramsl,indl) notations cum poly prv finite =
-  interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations cum poly prv finite
+let interp_mutual_inductive ~template udecl (paramsl,indl) notations cum ~poly prv finite =
+  interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations cum ~poly prv finite
 
 (* Very syntactical equality *)
 let eq_local_binders bl1 bl2 =
@@ -564,16 +564,16 @@ type uniform_inductive_flag =
   | UniformParameters
   | NonUniformParameters
 
-let do_mutual_inductive ~template udecl indl cum poly prv ~uniform finite =
+let do_mutual_inductive ~template udecl indl cum ~poly prv ~uniform finite =
   let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in
   (* Interpret the types *)
   let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in
-  let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns cum poly prv finite in
+  let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns cum ~poly prv finite in
   (* Declare the mutual inductive block with its associated schemes *)
   ignore (declare_mutual_inductive_with_eliminations mie pl impls);
   (* Declare the possible notations of inductive types *)
   List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns;
   (* Declare the coercions *)
-  List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false poly) coes;
+  List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes;
   (* If positivity is assumed declares itself as unsafe. *)
   if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else ()
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 2d6ecf48ef..a77cd66a33 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -26,7 +26,7 @@ type uniform_inductive_flag =
 val do_mutual_inductive :
   template:bool option -> universe_decl_expr option ->
   (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag ->
-  polymorphic -> private_flag -> uniform:uniform_inductive_flag ->
+  poly:bool -> private_flag -> uniform:uniform_inductive_flag ->
   Declarations.recursivity_kind -> unit
 
 (************************************************************************)
@@ -75,5 +75,5 @@ val extract_mutual_inductive_declaration_components :
 val interp_mutual_inductive :
   template:bool option -> universe_decl_expr option -> structured_inductive_expr ->
   decl_notation list -> cumulative_inductive_flag ->
-  polymorphic -> private_flag -> Declarations.recursivity_kind ->
+  poly:bool -> private_flag -> Declarations.recursivity_kind ->
   mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list
diff --git a/vernac/record.ml b/vernac/record.ml
index 9e3353bc54..268c778674 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -367,7 +367,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags f
 	    Impargs.maybe_declare_manual_implicits false refi impls;
             if flags.pf_subclass then begin
 	      let cl = Class.class_of_global (IndRef indsp) in
-	        Class.try_add_new_coercion_with_source refi ~local:false poly ~source:cl
+                Class.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl
 	    end;
 	    let i = if is_local_assum decl then i+1 else i in
 	      (Some kn::sp_projs, i, Projection term::subst)
@@ -470,7 +470,7 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki
     let cstr = (rsp, 1) in
     let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
     let build = ConstructRef cstr in
-    let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
+    let () = if is_coe then Class.try_add_new_coercion build ~local:false ~poly in
     let () = declare_structure_entry (cstr, List.rev kinds, List.rev sp_projs) in
     rsp
   in
@@ -680,7 +680,7 @@ let extract_record_data records =
 (* [fs] corresponds to fields and [ps] to parameters; [coers] is a
    list telling if the corresponding fields must me declared as coercions
    or subinstances. *)
-let definition_structure udecl kind ~template cum poly finite records =
+let definition_structure udecl kind ~template cum ~poly finite records =
   let () = check_unique_names records in
   let () = check_priorities kind records in
   let ps, data = extract_record_data records in
diff --git a/vernac/record.mli b/vernac/record.mli
index 11d9a833e2..d0164572f3 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -31,15 +31,18 @@ val declare_projections :
 
 val declare_structure_entry : Recordops.struc_tuple -> unit
 
-val definition_structure :
-  universe_decl_expr option -> inductive_kind -> template:bool option ->
-  Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
-  Declarations.recursivity_kind ->
-  (coercion_flag *
-  Names.lident *
-  local_binder_expr list *
-  (local_decl_expr * record_field_attr) list *
-  Id.t * constr_expr option) list ->
-  GlobRef.t list
+val definition_structure
+  :  universe_decl_expr option
+  -> inductive_kind
+  -> template:bool option
+  -> Decl_kinds.cumulative_inductive_flag
+  -> poly:bool
+  -> Declarations.recursivity_kind
+  -> (coercion_flag *
+      Names.lident *
+      local_binder_expr list *
+      (local_decl_expr * record_field_attr) list *
+      Id.t * constr_expr option) list
+  -> GlobRef.t list
 
 val declare_existing_class : GlobRef.t -> unit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 697dca788d..55fff432d5 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -584,13 +584,13 @@ let start_proof_and_print ~program_mode ~poly ?hook ~scope ~kind l =
   in
   start_lemma_com ~program_mode ?inference_hook ?hook ~poly ~scope ~kind l
 
-let vernac_definition_hook p = function
+let vernac_definition_hook ~poly = function
 | Coercion ->
-  Some (Class.add_coercion_hook p)
+  Some (Class.add_coercion_hook ~poly)
 | CanonicalStructure ->
   Some (DeclareDef.Hook.make (fun _ _ _ -> Canonical.declare_canonical_structure))
 | SubClass ->
-  Some (Class.add_subclass_hook p)
+  Some (Class.add_subclass_hook ~poly)
 | _ -> None
 
 let fresh_name_for_anonymous_theorem () =
@@ -613,7 +613,7 @@ let vernac_definition_name lid local =
 let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
   let open DefAttributes in
   let local = enforce_locality_exp atts.locality discharge in
-  let hook = vernac_definition_hook atts.polymorphic kind in
+  let hook = vernac_definition_hook ~poly:atts.polymorphic kind in
   let program_mode = atts.program in
   let poly = atts.polymorphic in
   let name = vernac_definition_name lid local in
@@ -622,7 +622,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
 let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt =
   let open DefAttributes in
   let scope = enforce_locality_exp atts.locality discharge in
-  let hook = vernac_definition_hook atts.polymorphic kind in
+  let hook = vernac_definition_hook ~poly:atts.polymorphic kind in
   let program_mode = atts.program in
   let name = vernac_definition_name lid scope in
   let red_option = match red_option with
@@ -726,7 +726,7 @@ let vernac_record ~template udecl cum k poly finite records =
     coe, id, binders, cfs, const, sort
   in
   let records = List.map map records in
-  ignore(Record.definition_structure ~template udecl k is_cumulative poly finite records)
+  ignore(Record.definition_structure ~template udecl k is_cumulative ~poly finite records)
 
 let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) =
   match indl with
@@ -826,7 +826,7 @@ let vernac_inductive ~atts cum lo finite indl =
     let indl = List.map unpack indl in
     let is_cumulative = should_treat_as_cumulative cum poly in
     let uniform = should_treat_as_uniform () in
-    ComInductive.do_mutual_inductive ~template udecl indl is_cumulative poly lo ~uniform finite
+    ComInductive.do_mutual_inductive ~template udecl indl is_cumulative ~poly lo ~uniform finite
   else
     user_err (str "Mixed record-inductive definitions are not allowed")
 (*
@@ -902,14 +902,14 @@ let vernac_universe ~poly l =
     user_err ~hdr:"vernac_universe"
 		 (str"Polymorphic universes can only be declared inside sections, " ++
 		  str "use Monomorphic Universe instead");
-  Declare.do_universe poly l
+  Declare.do_universe ~poly l
 
 let vernac_constraint ~poly l =
   if poly && not (Lib.sections_are_opened ()) then
     user_err ~hdr:"vernac_constraint"
 		 (str"Polymorphic universe constraints can only be declared"
 		  ++ str " inside sections, use Monomorphic Constraint instead");
-  Declare.do_constraint poly l
+  Declare.do_constraint ~poly l
 
 (**********************)
 (* Modules            *)
@@ -1089,62 +1089,62 @@ let vernac_canonical r =
   Canonical.declare_canonical_structure (smart_global r)
 
 let vernac_coercion ~atts ref qids qidt =
-  let local, polymorphic = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
+  let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
   let local = enforce_locality local in
   let target = cl_of_qualid qidt in
   let source = cl_of_qualid qids in
   let ref' = smart_global ref in
-  Class.try_add_new_coercion_with_target ref' ~local polymorphic ~source ~target;
+  Class.try_add_new_coercion_with_target ref' ~local ~poly ~source ~target;
   Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion")
 
 let vernac_identity_coercion ~atts id qids qidt =
-  let local, polymorphic = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
+  let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
   let local = enforce_locality local in
   let target = cl_of_qualid qidt in
   let source = cl_of_qualid qids in
-  Class.try_add_new_identity_coercion id ~local polymorphic ~source ~target
+  Class.try_add_new_identity_coercion id ~local ~poly ~source ~target
 
 (* Type classes *)
 
 let vernac_instance_program ~atts name bl t props info =
   Dumpglob.dump_constraint (fst name) false "inst";
-  let (program, locality), polymorphic =
+  let (program, locality), poly =
     Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts
   in
   let global = not (make_section_locality locality) in
-  let _id : Id.t = Classes.new_instance_program ~global polymorphic name bl t props info in
+  let _id : Id.t = Classes.new_instance_program ~global ~poly name bl t props info in
   ()
 
 let vernac_instance_interactive ~atts name bl t info =
   Dumpglob.dump_constraint (fst name) false "inst";
-  let (program, locality), polymorphic =
+  let (program, locality), poly =
     Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts
   in
   let global = not (make_section_locality locality) in
   let _id, pstate =
-    Classes.new_instance_interactive ~global polymorphic name bl t info in
+    Classes.new_instance_interactive ~global ~poly name bl t info in
   pstate
 
 let vernac_instance ~atts name bl t props info =
   Dumpglob.dump_constraint (fst name) false "inst";
-  let (program, locality), polymorphic =
+  let (program, locality), poly =
     Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts
   in
   let global = not (make_section_locality locality) in
   let _id : Id.t =
-    Classes.new_instance ~global polymorphic name bl t props info in
+    Classes.new_instance ~global ~poly name bl t props info in
   ()
 
 let vernac_declare_instance ~atts id bl inst pri =
   Dumpglob.dump_definition (fst id) false "inst";
-  let (program, locality), polymorphic =
+  let (program, locality), poly =
     Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts
   in
   let global = not (make_section_locality locality) in
-  Classes.declare_new_instance ~program_mode:program ~global polymorphic id bl inst pri
+  Classes.declare_new_instance ~program_mode:program ~global ~poly id bl inst pri
 
 let vernac_context ~poly l =
-  if not (ComAssumption.context poly l) then Feedback.feedback Feedback.AddedAxiom
+  if not (ComAssumption.context ~poly l) then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_existing_instance ~section_local insts =
   let glob = not section_local in
@@ -1267,7 +1267,7 @@ let vernac_hints ~atts dbnames h =
   in
   let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
   let local = enforce_module_locality local in
-  Hints.add_hints ~local dbnames (Hints.interp_hints poly h)
+  Hints.add_hints ~local dbnames (Hints.interp_hints ~poly h)
 
 let vernac_syntactic_definition ~atts lid x compat =
   let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in