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

31 files changed, 196 insertions, 182 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
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 201d953692..bb4e745fe9 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1506,7 +1506,7 @@ let do_build_inductive
   let _time2 = System.get_time () in
   try
     with_full_print
-      (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds false false false ~uniform:ComInductive.NonUniformParameters))
+      (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds false ~poly:false false ~uniform:ComInductive.NonUniformParameters))
       Declarations.Finite
   with
     | UserError(s,msg) as e ->
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 49d8ab4e23..1e2b23bf96 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -328,7 +328,7 @@ let add_rewrite_hint ~poly bases ort t lcsr =
         if poly then ctx
 	else (* This is a global universe context that shouldn't be
 	        refreshed at every use of the hint, declare it globally. *)
-	  (Declare.declare_universe_context false ctx;
+          (Declare.declare_universe_context ~poly:false ctx;
            Univ.ContextSet.empty)
     in
       CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 8d95c22529..9d928232c6 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1795,7 +1795,7 @@ let declare_an_instance n s args =
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
 let anew_instance atts binders (name,t) fields =
-  let _id = Classes.new_instance atts.polymorphic
+  let _id = Classes.new_instance ~poly:atts.polymorphic
       name binders t (true, CAst.make @@ CRecord (fields))
       ~global:atts.global ~generalize:false Hints.empty_hint_info
   in
@@ -2023,7 +2023,7 @@ let add_morphism atts binders m s n =
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
   let _id, lemma = Classes.new_instance_interactive
-      ~global:atts.global atts.polymorphic
+      ~global:atts.global ~poly:atts.polymorphic
       instance_name binders instance_t
       ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info
   in
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 9bbe339770..33798c43c8 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -153,7 +153,7 @@ let decl_constant na univs c =
   let open Constr in
   let vars = CVars.universes_of_constr c in
   let univs = UState.restrict_universe_context univs vars in
-  let () = Declare.declare_universe_context false univs in
+  let () = Declare.declare_universe_context ~poly:false univs in
   let types = (Typeops.infer (Global.env ()) c).uj_type in
   let univs = Monomorphic_entry Univ.ContextSet.empty in
   mkConst(declare_constant (Id.of_string na) 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index d1d20b9efe..5f8a073bd1 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -13,7 +13,6 @@
 open Names
 open Constr
 open Environ
-open Decl_kinds
 
 (** {6 ... } *)
 
@@ -67,7 +66,7 @@ val build_constant_by_tactic
   -> unit Proofview.tactic
   -> Evd.side_effects Proof_global.proof_entry * bool * UState.t
 
-val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic ->
+val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:bool ->
   EConstr.types -> unit Proofview.tactic ->
   constr * bool * UState.t
 
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 339d4de2a0..499e7a63d7 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -69,7 +69,7 @@ let auto_unif_flags =
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
-let connect_hint_clenv poly (c, _, ctx) clenv gl =
+let connect_hint_clenv ~poly (c, _, ctx) clenv gl =
   (* [clenv] has been generated by a hint-making function, so the only relevant
      data in its evarmap is the set of metas. The [evar_reset_evd] function
      below just replaces the metas of sigma by those coming from the clenv. *)
@@ -95,22 +95,22 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
       { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
   in clenv, c
 
-let unify_resolve poly flags ((c : raw_hint), clenv) =
+let unify_resolve ~poly flags ((c : raw_hint), clenv) =
   Proofview.Goal.enter begin fun gl ->
-  let clenv, c = connect_hint_clenv poly c clenv gl in
+  let clenv, c = connect_hint_clenv ~poly c clenv gl in
   let clenv = clenv_unique_resolver ~flags clenv gl in
   Clenvtac.clenv_refine clenv
   end
 
-let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h
+let unify_resolve_nodelta poly h = unify_resolve ~poly auto_unif_flags h
 
-let unify_resolve_gen poly = function
+let unify_resolve_gen ~poly = function
   | None -> unify_resolve_nodelta poly
-  | Some flags -> unify_resolve poly flags
+  | Some flags -> unify_resolve ~poly flags
 
 let exact poly (c,clenv) =
   Proofview.Goal.enter begin fun gl ->
-    let clenv', c = connect_hint_clenv poly c clenv gl in
+    let clenv', c = connect_hint_clenv ~poly c clenv gl in
     Tacticals.New.tclTHEN
     (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
     (exact_check c)
@@ -378,12 +378,12 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
 
 and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) =
   let tactic = function
-    | Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl)
+    | Res_pf (c,cl) -> unify_resolve_gen ~poly flags (c,cl)
     | ERes_pf _ -> Proofview.Goal.enter (fun gl -> Tacticals.New.tclZEROMSG (str "eres_pf"))
     | Give_exact (c, cl)  -> exact poly (c, cl)
     | Res_pf_THEN_trivial_fail (c,cl) ->
       Tacticals.New.tclTHEN
-        (unify_resolve_gen poly flags (c,cl))
+        (unify_resolve_gen ~poly flags (c,cl))
 	(* With "(debug) trivial", we shouldn't end here, and
 	   with "debug auto" we don't display the details of inner trivial *)
         (trivial_fail_db (no_dbg dbg) (not (Option.is_empty flags)) db_list local_db)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index a834b4b12d..5ae63be539 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -14,7 +14,6 @@ open Names
 open EConstr
 open Clenv
 open Pattern
-open Decl_kinds
 open Hints
 open Tactypes
 
@@ -24,11 +23,11 @@ val default_search_depth : int ref
 
 val auto_flags_of_state : TransparentState.t -> Unification.unify_flags
 
-val connect_hint_clenv : polymorphic -> raw_hint -> clausenv ->
-  Proofview.Goal.t -> clausenv * constr
+val connect_hint_clenv
+  : poly:bool -> raw_hint -> clausenv -> Proofview.Goal.t -> clausenv * constr
 
 (** Try unification with the precompiled clause, then use registered Apply *)
-val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic
+val unify_resolve : poly:bool -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic
 
 (** [ConclPattern concl pat tacast]:
    if the term concl matches the pattern pat, (in sense of
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index b0fb47726a..303ddacb67 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -204,11 +204,11 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' =
   end
 
 let unify_e_resolve poly flags = begin fun gls (c,_,clenv) ->
-  let clenv', c = connect_hint_clenv poly c clenv gls in
+  let clenv', c = connect_hint_clenv ~poly c clenv gls in
   clenv_unique_resolver_tac true ~flags clenv' end
 
 let unify_resolve poly flags = begin fun gls (c,_,clenv) ->
-  let clenv', _ = connect_hint_clenv poly c clenv gls in
+  let clenv', _ = connect_hint_clenv ~poly c clenv gls in
   clenv_unique_resolver_tac false ~flags clenv'
   end
 
@@ -536,7 +536,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
             (List.map_append
              (fun (path,info,c) ->
               make_resolves env sigma ~name:(PathHints path)
-                  (true,false,not !Flags.quiet) info false
+                  (true,false,not !Flags.quiet) info ~poly:false
                  (IsConstr (EConstr.of_constr c,Univ.ContextSet.empty)))
                hints)
         else []
@@ -544,8 +544,8 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
         (hints @ List.map_filter
          (fun f -> try Some (f (c, cty, Univ.ContextSet.empty))
            with Failure _ | UserError _ -> None)
-         [make_exact_entry ~name env sigma pri false;
-          make_apply_entry ~name env sigma flags pri false])
+         [make_exact_entry ~name env sigma pri ~poly:false;
+          make_apply_entry ~name env sigma flags pri ~poly:false])
     else []
 
 let make_hints g (modes,st) only_classes sign =
diff --git a/tactics/declare.ml b/tactics/declare.ml
index 02253e70bf..081c3a4b6a 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -98,7 +98,7 @@ let cache_constant ((sp,kn), obj) =
   assert (Constant.equal kn' (Constant.make1 kn));
   Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn));
   let cst = Global.lookup_constant kn' in
-  add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps;
+  add_section_constant ~poly:(Declareops.constant_is_polymorphic cst) kn' cst.const_hyps;
   add_constant_kind (Constant.make1 kn) obj.cst_kind
 
 let discharge_constant ((sp, kn), obj) =
@@ -264,7 +264,7 @@ let declare_definition ?(internal=UserIndividualRequest)
 (** Declaration of section variables and local definitions *)
 type section_variable_entry =
   | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
-  | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
+  | SectionLocalAssum of types Univ.in_universe_context_set * bool (* polymorphic *) * bool (* Implicit status *)
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
 
@@ -307,7 +307,7 @@ let cache_variable ((sp,_),o) =
       Explicit, de.proof_entry_opaque,
       poly, univs in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
-  add_section_variable id impl poly ctx;
+  add_section_variable ~name:id ~kind:impl ~poly ctx;
   add_variable_data id (p,opaq,ctx,poly,mk)
 
 let discharge_variable (_,o) = match o with
@@ -376,7 +376,7 @@ let cache_inductive ((sp,kn),mie) =
   let kn' = Global.add_mind id mie in
   assert (MutInd.equal kn' (MutInd.make1 kn));
   let mind = Global.lookup_mind kn' in
-  add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
+  add_section_kn ~poly:(Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
 
 let discharge_inductive ((sp,kn),mie) =
@@ -527,7 +527,7 @@ let input_universe_context : Univ.ContextSet.t -> Libobject.obj =
     ~cache:(fun (na, uctx) -> Global.push_context_set false uctx)
     ~discharge:(fun (_, x) -> Some x)
 
-let declare_universe_context poly ctx =
+let declare_universe_context ~poly ctx =
   if poly then
     (Global.push_context_set true ctx; Lib.add_section_context ctx)
   else
@@ -607,7 +607,7 @@ let declare_univ_binders gr pl =
     in
     Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs))
 
-let do_universe poly l =
+let do_universe ~poly l =
   let in_section = Lib.sections_are_opened () in
   let () =
     if poly && not in_section then
@@ -618,11 +618,11 @@ let do_universe poly l =
   let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx)
       Univ.LSet.empty l, Univ.Constraint.empty
   in
-  let () = declare_universe_context poly ctx in
+  let () = declare_universe_context ~poly ctx in
   let src = if poly then BoundUniv else UnqualifiedUniv in
   Lib.add_anonymous_leaf (input_univ_names (src, l))
 
-let do_constraint poly l =
+let do_constraint ~poly l =
   let open Univ in
   let u_of_id x =
     let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in
@@ -649,4 +649,4 @@ let do_constraint poly l =
     Constraint.empty l
   in
   let uctx = ContextSet.add_constraints constraints ContextSet.empty in
-  declare_universe_context poly uctx
+  declare_universe_context ~poly uctx
diff --git a/tactics/declare.mli b/tactics/declare.mli
index bdb5af7430..247c92bc5b 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -24,7 +24,7 @@ open Decl_kinds
 
 type section_variable_entry =
   | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
-  | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
+  | SectionLocalAssum of types Univ.in_universe_context_set * bool (* polymorphic *) * bool (* Implicit status *)
 
 type 'a constant_entry =
   | DefinitionEntry of 'a Proof_global.proof_entry
@@ -94,7 +94,7 @@ val exists_name : Id.t -> bool
 (** Global universe contexts, names and constraints *)
 val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
 
-val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
+val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
 
-val do_universe : polymorphic -> lident list -> unit
-val do_constraint : polymorphic -> Glob_term.glob_constraint list -> unit
+val do_universe : poly:bool -> lident list -> unit
+val do_constraint : poly:bool -> Glob_term.glob_constraint list -> unit
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index ac6253cf40..cc3e78f3b8 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -113,7 +113,7 @@ let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
 
 let unify_e_resolve poly flags (c,clenv) =
   Proofview.Goal.enter begin fun gl ->
-      let clenv', c = connect_hint_clenv poly c clenv gl in
+      let clenv', c = connect_hint_clenv ~poly c clenv gl in
       let clenv' = clenv_unique_resolver ~flags clenv' gl in
       Proofview.tclTHEN
         (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
@@ -131,7 +131,7 @@ let hintmap_of sigma secvars hdc concl =
 
 let e_exact poly flags (c,clenv) =
   Proofview.Goal.enter begin fun gl ->
-    let clenv', c = connect_hint_clenv poly c clenv gl in
+    let clenv', c = connect_hint_clenv ~poly c clenv gl in
     Tacticals.New.tclTHEN
     (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
     (e_give_exact c)
@@ -168,7 +168,7 @@ and e_my_find_search env sigma db_list local_db secvars hdc concl =
       in
       (b,
         let tac = function
-        | Res_pf (term,cl) -> unify_resolve poly st (term,cl)
+        | Res_pf (term,cl) -> unify_resolve ~poly st (term,cl)
         | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl)
         | Give_exact (c,cl) -> e_exact poly st (c,cl)
         | Res_pf_THEN_trivial_fail (term,cl) ->
diff --git a/tactics/hints.ml b/tactics/hints.ml
index e824c4bd64..014e54158d 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -27,7 +27,6 @@ open Smartlocate
 open Termops
 open Inductiveops
 open Typing
-open Decl_kinds
 open Typeclasses
 open Pattern
 open Patternops
@@ -142,15 +141,22 @@ type raw_hint = constr * types * Univ.ContextSet.t
 
 type hint = (raw_hint * clausenv) hint_ast with_uid
 
-type 'a with_metadata = {
-  pri     : int;            (* A number lower is higher priority *)
-  poly    : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
-  pat     : constr_pattern option; (* A pattern for the concl of the Goal *)
-  name    : hints_path_atom; (* A potential name to refer to the hint *)
-  db : string option; (** The database from which the hint comes *)
-  secvars : Id.Pred.t; (* The set of section variables the hint depends on *)
-  code    : 'a;     (* the tactic to apply when the concl matches pat *)
-}
+type 'a with_metadata =
+  { pri     : int
+  (** A number lower is higher priority *)
+  ; poly    : bool
+  (** Is the hint polymorpic and hence should be refreshed at each application *)
+  ; pat     : constr_pattern option
+  (** A pattern for the concl of the Goal *)
+  ; name    : hints_path_atom
+  (** A potential name to refer to the hint *)
+  ; db : string option
+  (** The database from which the hint comes *)
+  ; secvars : Id.Pred.t
+  (** The set of section variables the hint depends on *)
+  ; code    : 'a
+  (** the tactic to apply when the concl matches pat *)
+  }
 
 type full_hint = hint with_metadata
 
@@ -792,7 +798,7 @@ let secvars_of_constr env sigma c =
 let secvars_of_global env gr =
   secvars_of_idset (vars_of_global env gr)
 
-let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) =
+let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) =
   let secvars = secvars_of_constr env sigma c in
   let cty = strip_outer_cast sigma cty in
     match EConstr.kind sigma cty with
@@ -813,7 +819,7 @@ let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) =
 	   db = None; secvars;
 	   code = with_uid (Give_exact (c, cty, ctx)); })
 
-let make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c, cty, ctx) =
+let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (c, cty, ctx) =
   let cty = if hnf then hnf_constr env sigma cty else cty in
   match EConstr.kind sigma cty with
   | Prod _ ->
@@ -887,18 +893,18 @@ let fresh_global_or_constr env sigma poly cr =
     else begin
       if isgr then
         warn_polymorphic_hint (pr_hint_term env sigma ctx cr);
-      Declare.declare_universe_context false ctx;
+      Declare.declare_universe_context ~poly:false ctx;
       (c, Univ.ContextSet.empty)
     end
 
-let make_resolves env sigma flags info poly ?name cr =
+let make_resolves env sigma flags info ~poly ?name cr =
   let c, ctx = fresh_global_or_constr env sigma poly cr in
   let cty = Retyping.get_type_of env sigma c in
   let try_apply f =
     try Some (f (c, cty, ctx)) with Failure _ -> None in
   let ents = List.map_filter try_apply
-			     [make_exact_entry env sigma info poly ?name;
-			      make_apply_entry env sigma flags info poly ?name]
+                             [make_exact_entry env sigma info ~poly ?name;
+                              make_apply_entry env sigma flags info ~poly ?name]
   in
   if List.is_empty ents then
     user_err ~hdr:"Hint"
@@ -912,7 +918,7 @@ let make_resolve_hyp env sigma decl =
   let hname = NamedDecl.get_id decl in
   let c = mkVar hname in
   try
-    [make_apply_entry env sigma (true, true, false) empty_hint_info false
+    [make_apply_entry env sigma (true, true, false) empty_hint_info ~poly:false
        ~name:(PathHints [VarRef hname])
        (c, NamedDecl.get_type decl, Univ.ContextSet.empty)]
   with
@@ -1178,7 +1184,7 @@ let add_resolves env sigma clist local dbnames =
       let r =
         List.flatten (List.map (fun (pri, poly, hnf, path, gr) ->
           make_resolves env sigma (true,hnf,not !Flags.quiet)
-            pri poly ~name:path gr) clist)
+            pri ~poly ~name:path gr) clist)
       in
       let hint = make_hint ~local dbname (AddHints r) in
       Lib.add_anonymous_leaf (inAutoHint hint))
@@ -1238,8 +1244,8 @@ type hnf = bool
 type nonrec hint_info = hint_info
 
 type hints_entry =
-  | HintsResolveEntry of (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list
-  | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list
+  | HintsResolveEntry of (hint_info * bool * hnf * hints_path_atom * hint_term) list
+  | HintsImmediateEntry of (hints_path_atom * bool * hint_term) list
   | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool
@@ -1286,7 +1292,7 @@ let prepare_hint check (poly,local) env init (sigma,c) =
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
     if poly then IsConstr (c', diff)
     else if local then IsConstr (c', diff)
-    else (Declare.declare_universe_context false diff;
+    else (Declare.declare_universe_context ~poly:false diff;
 	  IsConstr (c', Univ.ContextSet.empty))
 
 let project_hint ~poly pri l2r r =
@@ -1318,7 +1324,7 @@ let project_hint ~poly pri l2r r =
   let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
     (info,false,true,PathAny, IsGlobRef (Globnames.ConstRef c))
 
-let interp_hints poly =
+let interp_hints ~poly =
   fun h ->
   let env = Global.env () in
   let sigma = Evd.from_env env in
@@ -1417,7 +1423,7 @@ let expand_constructor_hints env sigma lems =
 let constructor_hints env sigma eapply lems =
   let lems = expand_constructor_hints env sigma lems in
   List.map_append (fun (poly, lem) ->
-      make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems
+      make_resolves env sigma (eapply,true,false) empty_hint_info ~poly lem) lems
 
 let make_local_hint_db env sigma ts eapply lems =
   let map c = c env sigma in
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 839ef31189..4c82a068b1 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -12,7 +12,6 @@ open Util
 open Names
 open EConstr
 open Environ
-open Decl_kinds
 open Evd
 open Tactypes
 open Clenv
@@ -54,15 +53,22 @@ type 'a hints_path_atom_gen =
 type hints_path_atom = GlobRef.t hints_path_atom_gen
 type hint_db_name = string
 
-type 'a with_metadata = private {
-  pri   : int;            (** A number between 0 and 4, 4 = lower priority *)
-  poly  : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
-  pat   : constr_pattern option; (** A pattern for the concl of the Goal *)
-  name  : hints_path_atom; (** A potential name to refer to the hint *) 
-  db    : hint_db_name option;
-  secvars : Id.Pred.t; (** The section variables this hint depends on, as a predicate *)
-  code    : 'a; (** the tactic to apply when the concl matches pat *)
-}
+type 'a with_metadata = private
+  { pri     : int
+  (** A number lower is higher priority *)
+  ; poly    : bool
+  (** Is the hint polymorpic and hence should be refreshed at each application *)
+  ; pat     : constr_pattern option
+  (** A pattern for the concl of the Goal *)
+  ; name    : hints_path_atom
+  (** A potential name to refer to the hint *)
+  ; db : string option
+  (** The database from which the hint comes *)
+  ; secvars : Id.Pred.t
+  (** The set of section variables the hint depends on *)
+  ; code    : 'a
+  (** the tactic to apply when the concl matches pat *)
+  }
 
 type full_hint = hint with_metadata
 
@@ -176,9 +182,8 @@ type hint_term =
   | IsConstr of constr * Univ.ContextSet.t
 
 type hints_entry =
-  | HintsResolveEntry of
-    (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list
-  | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list
+  | HintsResolveEntry of (hint_info * bool * hnf * hints_path_atom * hint_term) list
+  | HintsImmediateEntry of (hints_path_atom * bool * hint_term) list
   | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool
@@ -202,7 +207,7 @@ val current_db_names : unit -> String.Set.t
 
 val current_pure_db : unit -> hint_db list
 
-val interp_hints : polymorphic -> hints_expr -> hints_entry
+val interp_hints : poly:bool -> hints_expr -> hints_entry
 
 val add_hints : local:bool -> hint_db_name list -> hints_entry -> unit
 
@@ -219,7 +224,7 @@ val prepare_hint : bool (* Check no remaining evars *) ->
    [hint_pattern] is the hint's desired pattern, it is inferred if not specified
 *)
 
-val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hints_path_atom ->
+val make_exact_entry : env -> evar_map -> hint_info -> poly:bool -> ?name:hints_path_atom ->
   (constr * types * Univ.ContextSet.t) -> hint_entry
 
 (** [make_apply_entry (eapply,hnf,verbose) info (c,cty,ctx))].
@@ -237,7 +242,7 @@ val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hint
 *)
 
 val make_apply_entry :
-  env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom ->
+  env -> evar_map -> bool * bool * bool -> hint_info -> poly:bool -> ?name:hints_path_atom ->
   (constr * types * Univ.ContextSet.t) -> hint_entry
 
 (** A constr which is Hint'ed will be:
@@ -248,7 +253,7 @@ val make_apply_entry :
          has missing arguments. *)
 
 val make_resolves :
-  env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom ->
+  env -> evar_map -> bool * bool * bool -> hint_info -> poly:bool -> ?name:hints_path_atom ->
   hint_term -> hint_entry list
 
 (** [make_resolve_hyp hname htyp].
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