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

32 files changed, 331 insertions, 203 deletions

diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 328ddd0cd..637744df3 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -546,7 +546,8 @@ let rec tmpp v loc =
         | DefineBody (_, None  , ce, None) -> ce
         | DefineBody (_, Some _, ce, Some _) -> ce
         | DefineBody (_, None  , ce, Some _) -> ce in
-      let str_dk = Kindops.string_of_definition_kind (l, false, dk) in
+      let def_kind = { locality = l; polymorphic = false; object_kind = dk } in
+      let str_dk = Kindops.string_of_definition_kind def_kind in
       let str_id = Id.to_string id in
       (xmlDef str_dk str_id loc [pp_expr e])
   | VernacStartTheoremProof (tk, [ Some ((_,id),_), ([], statement, None) ], b) ->
diff --git a/intf/decl_kinds.mli b/intf/decl_kinds.mli
index 6a4e18833..29972f2f4 100644
--- a/intf/decl_kinds.mli
+++ b/intf/decl_kinds.mli
@@ -49,9 +49,13 @@ type assumption_object_kind = Definitional | Logical | Conjectural
    Logical      |  Hypothesis | Axiom
 
 *)
-type assumption_kind = locality * polymorphic * assumption_object_kind
+type 'a declaration_kind = { locality : locality;
+                             polymorphic : bool;
+                             object_kind : 'a }
 
-type definition_kind = locality * polymorphic * definition_object_kind
+type assumption_kind = assumption_object_kind declaration_kind
+
+type definition_kind = definition_object_kind declaration_kind
 
 (** Kinds used in proofs *)
 
@@ -59,7 +63,7 @@ type goal_object_kind =
   | DefinitionBody of definition_object_kind
   | Proof of theorem_kind
 
-type goal_kind = locality * polymorphic * goal_object_kind
+type goal_kind = goal_object_kind declaration_kind
 
 (** Kinds used in library *)
 
diff --git a/library/declare.ml b/library/declare.ml
index cc8415cf4..36a58629e 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 7824506da..760bf437b 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 2952c258a..1e9afe968 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 1ca7f8946..e84a6376b 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 21b1bec33..3d737e5ac 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 749cc4ff3..954889fb6 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 092643c2d..e905ee57e 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
 
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index a332e2871..ef9d49998 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1755,7 +1755,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 global binders instance fields =
-  new_instance (Flags.is_universe_polymorphism ()) 
+  new_instance ~polymorphic:(Flags.is_universe_polymorphism ()) 
     binders instance (Some (true, CRecord (Loc.ghost,fields)))
     ~global ~generalize:false ~refine:false None
 
@@ -1828,7 +1828,7 @@ let proper_projection r ty =
     it_mkLambda_or_LetIn app ctx
 
 let declare_projection n instance_id r =
-  let poly = Global.is_polymorphic r in
+  let polymorphic = Global.is_polymorphic r in
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let sigma,c = Evd.fresh_global env sigma r in
@@ -1858,7 +1858,7 @@ let declare_projection n instance_id r =
   let typ = it_mkProd_or_LetIn typ ctx in
   let pl, ctx = Evd.universe_context sigma in
   let cst = 
-    Declare.definition_entry ~types:typ ~poly ~univs:ctx term
+    Declare.definition_entry ~types:typ ~polymorphic ~univs:ctx term
   in
     ignore(Declare.declare_constant n 
 	   (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
@@ -1942,8 +1942,9 @@ let add_morphism_infer glob m n =
 			poly (ConstRef cst));
 	declare_projection n instance_id (ConstRef cst)
     else
-      let kind = Decl_kinds.Global, poly, 
-	Decl_kinds.DefinitionBody Decl_kinds.Instance 
+      let kind = { locality = Decl_kinds.Global;
+                   polymorphic = poly;
+                   object_kind = Decl_kinds.DefinitionBody Decl_kinds.Instance }
       in
       let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
       let hook _ = function
@@ -1962,7 +1963,7 @@ let add_morphism_infer glob m n =
 
 let add_morphism glob binders m s n =
   init_setoid ();
-  let poly = Flags.is_universe_polymorphism () in
+  let polymorphic = Flags.is_universe_polymorphism () in
   let instance_id = add_suffix n "_Proper" in
   let instance =
     (((Loc.ghost,Name instance_id),None), Explicit,
@@ -1971,7 +1972,7 @@ let add_morphism glob binders m s n =
 	     [cHole; s; m]))
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
-    ignore(new_instance ~global:glob poly binders instance 
+    ignore(new_instance ~global:glob ~polymorphic binders instance 
 	     (Some (true, CRecord (Loc.ghost,[])))
 	      ~generalize:false ~tac ~hook:(declare_projection n instance_id) None)
 
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index e39d17b52..12fd8359a 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -22,7 +22,10 @@ let start_deriving f suchthat lemma =
 
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let kind = Decl_kinds.(Global,false,DefinitionBody Definition) in
+  let kind = Decl_kinds.{ locality = Global;
+                          polymorphic = false;
+                          object_kind = DefinitionBody Definition }
+  in
 
   (** create a sort variable for the type of [f] *)
   (* spiwack: I don't know what the rigidity flag does, picked the one
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 527f4f0b1..bba7b3c59 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -996,7 +996,9 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
       Ensures by: obvious
       i*)
     (mk_equation_id f_id)
-    (Decl_kinds.Global, Flags.is_universe_polymorphism (), (Decl_kinds.Proof Decl_kinds.Theorem))
+    Decl_kinds.{ locality = Global;
+                 polymorphic = Flags.is_universe_polymorphism ();
+                 object_kind = Proof Theorem }
     evd
   lemma_type
   (Lemmas.mk_hook (fun _ _ -> ()));
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index cc699e5d3..4f5f167c2 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -288,7 +288,9 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   begin
     Lemmas.start_proof
       new_princ_name
-      (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem))
+      Decl_kinds.{ locality = Decl_kinds.Global;
+                   polymorphic = Flags.is_universe_polymorphism ();
+                   object_kind = Decl_kinds.Proof Decl_kinds.Theorem }
       !evd
       new_principle_type
       hook
@@ -339,7 +341,9 @@ let generate_functional_principle (evd: Evd.evar_map ref)
 	let evd',value = change_property_sort evd' s new_principle_type new_princ_name in
 	let evd' = fst (Typing.type_of ~refresh:true (Global.env ()) evd' value) in
 	(* Pp.msgnl (str "new principle := " ++ pr_lconstr value); *)
-	let ce = Declare.definition_entry ~poly:(Flags.is_universe_polymorphism ()) ~univs:(snd (Evd.universe_context evd')) value in
+	let ce = Declare.definition_entry ~polymorphic:(Flags.is_universe_polymorphism ())
+                                          ~univs:(snd (Evd.universe_context evd')) value
+        in
 	ignore(
 	  Declare.declare_constant
 	    name
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 99b04898b..efbc1507f 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -395,7 +395,9 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
       let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in 
       Command.do_definition
 	fname
-	(Decl_kinds.Global,(Flags.is_universe_polymorphism ()),Decl_kinds.Definition) pl
+        { locality = Decl_kinds.Global;
+          polymorphic = Flags.is_universe_polymorphism ();
+          object_kind = Decl_kinds.Definition } pl
 	bl None body (Some ret_type) (Lemmas.mk_hook (fun _ _ -> ()));
        let evd,rev_pconstants =
 	 List.fold_left
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index a45effb16..8c6673732 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -148,17 +148,18 @@ let get_locality = function
 | Local -> true
 | Global -> false
 
-let save with_clean id const (locality,_,kind) hook =
+let save with_clean id const goal_kind hook =
   let fix_exn = Future.fix_exn_of const.const_entry_body in
+  let locality = goal_kind.locality in
   let l,r = match locality with
     | Discharge when Lib.sections_are_opened () ->
-        let k = Kindops.logical_kind_of_goal_kind kind in
+        let k = Kindops.logical_kind_of_goal_kind goal_kind.object_kind in
 	let c = SectionLocalDef const in
 	let _ = declare_variable id (Lib.cwd(), c, k) in
 	(Local, VarRef id)
     | Discharge | Local | Global ->
         let local = get_locality locality in
-        let k = Kindops.logical_kind_of_goal_kind kind in
+        let k = Kindops.logical_kind_of_goal_kind goal_kind.object_kind in
         let kn = declare_constant id ~local (DefinitionEntry const, k) in
 	(locality, ConstRef kn)
   in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index c8b4e4833..6d042b3a4 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -832,7 +832,9 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 let (typ,_) = lemmas_types_infos.(i) in 
 	 Lemmas.start_proof
 	   lem_id
-	   (Decl_kinds.Global,Flags.is_universe_polymorphism (),((Decl_kinds.Proof Decl_kinds.Theorem)))
+           Decl_kinds.{ locality = Decl_kinds.Global;
+                        polymorphic = Flags.is_universe_polymorphism ();
+                        object_kind = Decl_kinds.Proof Decl_kinds.Theorem }
            !evd
 	   typ
            (Lemmas.mk_hook (fun _ _ -> ()));
@@ -893,10 +895,13 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	     Ensures by: obvious
 	   i*)
 	 let lem_id = mk_complete_id f_id in
-	 Lemmas.start_proof lem_id
-	   (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma
-	 (fst lemmas_types_infos.(i))
-           (Lemmas.mk_hook (fun _ _ -> ()));
+         Lemmas.start_proof lem_id
+                            Decl_kinds.{ locality = Decl_kinds.Global;
+                                         polymorphic = Flags.is_universe_polymorphism ();
+                                         object_kind = Decl_kinds.Proof Decl_kinds.Theorem }
+                            sigma
+	                    (fst lemmas_types_infos.(i))
+                            (Lemmas.mk_hook (fun _ _ -> ()));
 	 ignore (Pfedit.by
 	   (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
 	      (proving_tac i)))) ;
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index f43251bc5..75495ed98 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1348,7 +1348,9 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
   in
   Lemmas.start_proof
     na
-    (Decl_kinds.Global, false (* FIXME *), Decl_kinds.Proof Decl_kinds.Lemma)
+    { locality = Decl_kinds.Global;
+      polymorphic = false (* FIXME *);
+      object_kind = Decl_kinds.Proof Decl_kinds.Lemma }
     sigma gls_type
     (Lemmas.mk_hook hook);
   if Indfun_common.is_strict_tcc  ()
@@ -1394,8 +1396,12 @@ let com_terminate
     hook =
   let start_proof ctx (tac_start:tactic) (tac_end:tactic) =
     let (evmap, env) = Lemmas.get_current_context() in
+    let goal_kind = { locality = Global;
+                      polymorphic = false; (* FIXME *)
+                      object_kind = Proof Lemma }
+    in
     Lemmas.start_proof thm_name
-      (Global, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
+      goal_kind ~sign:(Environ.named_context_val env)
       ctx (compute_terminate_type nb_args fonctional_ref) hook;
 
     ignore (by (Proofview.V82.tactic (observe_tac (str "starting_tac") tac_start)));
@@ -1445,7 +1451,11 @@ let (com_eqn : int -> Id.t ->
     let evmap = Evd.from_ctx (Evd.evar_universe_context evmap) in
     let f_constr = constr_of_global f_ref in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
-    (Lemmas.start_proof eq_name (Global, false, Proof Lemma)
+    let goal_kind = { locality = Global;
+                      polymorphic = false;
+                      object_kind = Proof Lemma }
+    in
+    (Lemmas.start_proof eq_name goal_kind
        ~sign:(Environ.named_context_val env)
        evmap
        equation_lemma_type
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 51fc289b4..9a8ad00d0 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -695,7 +695,8 @@ module Make
       | VernacDefinition (d,id,b) -> (* A verifier... *)
         let pr_def_token (l,dk) =
           let l = match l with Some x -> x | None -> Decl_kinds.Global in
-          keyword (Kindops.string_of_definition_kind (l,false,dk))
+          keyword (Kindops.string_of_definition_kind
+                     { locality = l; polymorphic = false; object_kind = dk })
         in
         let pr_reduce = function
           | None -> mt()
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 86c2b7a57..d55d6ce6b 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -147,7 +147,10 @@ open Decl_kinds
 
 let next = let n = ref 0 in fun () -> incr n; !n
 
-let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theorem) typ tac =
+let default_goal_kind =
+  { locality = Global; polymorphic = false; object_kind = Proof Theorem }
+
+let build_constant_by_tactic id ctx sign ?(goal_kind = default_goal_kind) typ tac =
   let evd = Evd.from_ctx ctx in
   let terminator = Proof_global.make_terminator (fun _ -> ()) in
   start_proof id goal_kind evd sign typ terminator;
@@ -161,10 +164,10 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo
     delete_current_proof ();
     iraise reraise
 
-let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac =
+let build_by_tactic ?(side_eff=true) env ctx ?(polymorphic=false) typ tac =
   let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
-  let gk = Global, poly, Proof Theorem in
+  let gk = { locality = Global; polymorphic; object_kind = Proof Theorem } in
   let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in
   let ce =
     if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index f2f4b11ed..aa01969b7 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -169,7 +169,7 @@ val build_constant_by_tactic :
   types -> unit Proofview.tactic -> 
   Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context
 
-val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic ->
+val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?polymorphic:polymorphic ->
   types -> unit Proofview.tactic -> 
   constr * bool * Evd.evar_universe_context
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 2956d623f..911d4ffbc 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -320,7 +320,7 @@ let constrain_variables init uctx =
 let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
   let { pid; section_vars; strength; proof; terminator; universe_binders } =
     cur_pstate () in
-  let poly = pi2 strength (* Polymorphic *) in
+  let poly = strength.Decl_kinds.polymorphic in
   let initial_goals = Proof.initial_goals proof in
   let initial_euctx = Proof.initial_euctx proof in
   let fpl, univs = Future.split2 fpl in
@@ -398,7 +398,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
 type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
 
 let return_proof ?(allow_partial=false) () =
- let { pid; proof; strength = (_,poly,_) } = cur_pstate () in
+ let { pid; proof; strength = { Decl_kinds.polymorphic }} = cur_pstate () in
  if allow_partial then begin
   let proofs = Proof.partial_proof proof in
   let _,_,_,_, evd = Proof.proof proof in
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 2ab3b9c59..004dd6801 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -191,11 +191,12 @@ let look_for_possibly_mutual_statements = function
 
 (* Saving a goal *)
 
-let save ?export_seff id const cstrs pl do_guard (locality,poly,kind) hook =
+let save ?export_seff id const cstrs pl do_guard
+         { locality; polymorphic; object_kind } hook =
   let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
   try
     let const = adjust_guardness_conditions const do_guard in
-    let k = Kindops.logical_kind_of_goal_kind kind in
+    let k = Kindops.logical_kind_of_goal_kind object_kind in
     let l,r = match locality with
       | Discharge when Lib.sections_are_opened () ->
           let c = SectionLocalDef const in
@@ -229,16 +230,20 @@ let compute_proof_name locality = function
   | None ->
       next_global_ident_away default_thm_id (Pfedit.get_all_proof_names ()), None
 
-let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,(_,imps))) =
+let save_remaining_recthms { locality; polymorphic; object_kind }
+                           norm ctx body opaq i ((id,pl),(t_i,(_,imps))) =
   let t_i = norm t_i in
   match body with
   | None ->
       (match locality with
       | Discharge ->
-          let impl = false in (* copy values from Vernacentries *)
+          let impl = Explicit in (* copy values from Vernacentries *)
           let k = IsAssumption Conjectural in
-          let c = SectionLocalAssum ((t_i,ctx),p,impl) in
-	  let _ = declare_variable id (Lib.cwd(),c,k) in
+          let c = SectionLocalAssum { type_context = (t_i,ctx);
+                                      polymorphic;
+                                      binding_kind = impl }
+          in
+          let _ = declare_variable id (Lib.cwd(),c,k) in
           (Discharge, VarRef id,imps)
       | Local | Global ->
           let k = IsAssumption Conjectural in
@@ -248,12 +253,12 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,
           | Discharge -> assert false
           in
           let ctx = Univ.ContextSet.to_context ctx in
-          let decl = (ParameterEntry (None,p,(t_i,ctx),None), k) in
+          let decl = (ParameterEntry (None,polymorphic,(t_i,ctx),None), k) in
           let kn = declare_constant id ~local decl in
           (locality,ConstRef kn,imps))
   | Some body ->
       let body = norm body in
-      let k = Kindops.logical_kind_of_goal_kind kind in
+      let k = Kindops.logical_kind_of_goal_kind object_kind in
       let rec body_i t = match kind_of_term t with
         | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
         | CoFix (0,decls) -> mkCoFix (i,decls)
@@ -264,7 +269,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,
       let body_i = body_i body in
       match locality with
       | Discharge ->
-          let const = definition_entry ~types:t_i ~opaque:opaq ~poly:p 
+          let const = definition_entry ~types:t_i ~opaque:opaq ~polymorphic 
 	    ~univs:(Univ.ContextSet.to_context ctx) body_i in
 	  let c = SectionLocalDef const in
 	  let _ = declare_variable id (Lib.cwd(), c, k) in
@@ -277,7 +282,7 @@ let save_remaining_recthms (locality,p,kind) norm ctx body opaq i ((id,pl),(t_i,
         | Discharge -> assert false
         in
         let const =
-	  Declare.definition_entry ~types:t_i ~poly:p ~univs:ctx ~opaque:opaq body_i
+	  Declare.definition_entry ~types:t_i ~polymorphic ~univs:ctx ~opaque:opaq body_i
 	in
         let kn = declare_constant id ~local (DefinitionEntry const, k) in
         (locality,ConstRef kn,imps)
@@ -303,7 +308,10 @@ let save_anonymous_with_strength ?export_seff proof kind save_ident =
   check_anonymity id save_ident;
   (* we consider that non opaque behaves as local for discharge *)
   save ?export_seff save_ident const cstrs pl do_guard
-      (Global, const.const_entry_polymorphic, Proof kind) hook
+       { locality = Global;
+         polymorphic = const.const_entry_polymorphic;
+         object_kind = Proof kind}
+       hook
 
 (* Admitted *)
 
@@ -314,9 +322,9 @@ let warn_let_as_axiom =
 
 let admit (id,k,e) pl hook () =
   let kn = declare_constant id (ParameterEntry e, IsAssumption Conjectural) in
-  let () = match k with
-  | Global, _, _ -> ()
-  | Local, _, _ | Discharge, _, _ -> warn_let_as_axiom id
+  let () = match k.locality with
+  | Global -> ()
+  | Local | Discharge -> warn_let_as_axiom id
   in
   let () = assumption_message id in
   Option.iter (Universes.register_universe_binders (ConstRef kn)) pl;
@@ -463,7 +471,7 @@ let start_proof_com kind thms hook =
     let t', imps' = interp_type_evars_impls ~impls env evdref t in
     evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref);
     let ids = List.map RelDecl.get_name ctx in
-      (compute_proof_name (pi1 kind) sopt,
+      (compute_proof_name kind.locality sopt,
       (nf_evar !evdref (it_mkProd_or_LetIn t' ctx),
        (ids, imps @ lift_implicits (List.length ids) imps'),
        guard)))
@@ -477,7 +485,7 @@ let start_proof_com kind thms hook =
     | Some l -> ignore (Evd.universe_context evd ?names:l)
   in
   let evd =
-    if pi2 kind then evd
+    if kind.polymorphic then evd
     else (* We fix the variables to ensure they won't be lowered to Set *)
       Evd.fix_undefined_variables evd
   in
@@ -512,7 +520,7 @@ let save_proof ?proof = function
             let typ = Option.get const_entry_type in
             let ctx = Evd.evar_context_universe_context (fst universes) in
             let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
-            Admitted(id, k, (sec_vars, pi2 k, (typ, ctx), None), universes)
+            Admitted(id, k, (sec_vars, k.polymorphic, (typ, ctx), None), universes)
         | None ->
             let pftree = Pfedit.get_pftreestate () in
             let id, k, typ = Pfedit.current_proof_statement () in
@@ -533,7 +541,7 @@ let save_proof ?proof = function
 	    let names = Pfedit.get_universe_binders () in
             let evd = Evd.from_ctx universes in
             let binders, ctx = Evd.universe_context ?names evd in
-            Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
+            Admitted(id,k,(sec_vars, k.polymorphic, (typ, ctx), None),
 		     (universes, Some binders))
       in
       Proof_global.apply_terminator (Proof_global.get_terminator ()) pe
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index d80e86241..c7b8e6cc0 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -233,7 +233,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
 
 let add_inversion_lemma name env sigma t sort dep inv_op =
   let invProof, ctx = inversion_scheme env sigma t sort dep inv_op in
-  let entry = definition_entry ~poly:(Flags.use_polymorphic_flag ())
+  let entry = definition_entry ~polymorphic:(Flags.use_polymorphic_flag ())
 			       ~univs:(snd ctx) invProof in
   let _ = declare_constant name (DefinitionEntry entry, IsProof Lemma) in
   ()
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 9d0e9f084..86c0b9dd5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -4888,7 +4888,9 @@ let anon_id = Id.of_string "anonymous"
 
 let tclABSTRACT name_op tac =
   let open Proof_global in
-  let default_gk = (Global, false, Proof Theorem) in
+  let default_gk =
+    { locality = Global; polymorphic = false; object_kind = Proof Theorem }
+  in
   let s, gk = match name_op with
     | Some s ->
       (try let _, gk, _ = current_proof_statement () in s, gk
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 0dc799014..9582015a0 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -180,7 +180,7 @@ let error_not_transparent source =
   user_err ~hdr:"build_id_coercion"
     (pr_class source ++ str " must be a transparent constant.")
 
-let build_id_coercion idf_opt source poly =
+let build_id_coercion idf_opt source ~polymorphic =
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let sigma, vs = match source with
@@ -221,7 +221,7 @@ let build_id_coercion idf_opt source poly =
   in
   let constr_entry = (* Cast is necessary to express [val_f] is identity *)
     DefinitionEntry
-      (definition_entry ~types:typ_f ~poly ~univs:(snd (Evd.universe_context sigma))
+      (definition_entry ~types:typ_f ~polymorphic ~univs:(snd (Evd.universe_context sigma))
 	 ~inline:true (mkCast (val_f, DEFAULTcast, typ_f)))
   in
   let decl = (constr_entry, IsDefinition IdentityCoercion) in
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index ad4a13c21..a0a8d2aaf 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -106,7 +106,7 @@ let instance_hook k pri global imps ?hook cst =
   Typeclasses.declare_instance pri (not global) cst;
   (match hook with Some h -> h cst | None -> ())
 
-let declare_instance_constant k pri global imps ?hook id pl poly evm term termtype =
+let declare_instance_constant k pri global imps ?hook id pl ~polymorphic evm term termtype =
   let kind = IsDefinition Instance in
   let evm = 
     let levels = Univ.LSet.union (Universes.universes_of_constr termtype) 
@@ -115,7 +115,7 @@ let declare_instance_constant k pri global imps ?hook id pl poly evm term termty
   in
   let pl, uctx = Evd.universe_context ?names:pl evm in
   let entry = 
-    Declare.definition_entry ~types:termtype ~poly ~univs:uctx term
+    Declare.definition_entry ~types:termtype ~polymorphic ~univs:uctx term
   in
   let cdecl = (DefinitionEntry entry, kind) in
   let kn = Declare.declare_constant id cdecl in
@@ -124,7 +124,7 @@ let declare_instance_constant k pri global imps ?hook id pl poly evm term termty
     instance_hook k pri global imps ?hook (ConstRef kn);
     id
 
-let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) poly ctx (instid, bk, cl) props
+let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~polymorphic ctx (instid, bk, cl) props
     ?(generalize=true)
     ?(tac:unit Proofview.tactic option) ?hook pri =
   let env = Global.env() in
@@ -197,7 +197,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
 	let pl, ctx = Evd.universe_context ?names:pl !evars in
 	let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
 	  (ParameterEntry 
-            (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
+            (None,polymorphic,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
 	in
 	  Universes.register_universe_binders (ConstRef cst) pl;
 	  instance_hook k pri global imps ?hook (ConstRef cst); id
@@ -294,9 +294,12 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
       let term = Option.map nf term in
 	if not (Evd.has_undefined evm) && not (Option.is_empty term) then
 	  declare_instance_constant k pri global imps ?hook id pl
-            poly evm (Option.get term) termtype
+            ~polymorphic evm (Option.get term) termtype
 	else if Flags.is_program_mode () || refine || Option.is_empty term then begin
-	  let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
+            let kind = { locality = Decl_kinds.Global;
+                         polymorphic;
+                         object_kind = Decl_kinds.DefinitionBody Decl_kinds.Instance }
+            in
 	    if Flags.is_program_mode () then
 	      let hook vis gr _ =
 		let cst = match gr with ConstRef kn -> kn | _ -> assert false in
@@ -313,8 +316,12 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
 	      in
               let hook = Lemmas.mk_hook hook in
 	      let ctx = Evd.evar_universe_context evm in
-		ignore (Obligations.add_definition id ?term:constr
- 			?pl typ ctx ~kind:(Global,poly,Instance) ~hook obls);
+              let kind = { locality = Global;
+                           polymorphic;
+                           object_kind = Instance }
+              in
+                ignore (Obligations.add_definition id ?term:constr
+ 			?pl typ ctx ~kind ~hook obls);
 		id
 	    else
 	      (Flags.silently 
@@ -390,8 +397,11 @@ let context poly l =
       | ExplByPos (_, Some id') -> Id.equal id id'
       | _ -> false
       in
-      let impl = List.exists test impls in
-      let decl = (Discharge, poly, Definitional) in
+      let impl = if List.exists test impls then Implicit else Explicit in
+      let decl = { locality = Discharge;
+                   polymorphic = poly;
+                   object_kind = Definitional }
+      in
       let nstatus =
         pi3 (Command.declare_assumption false decl (t, !uctx) [] [] impl
           Vernacexpr.NoInline (Loc.ghost, id))
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 7beb873e6..fc7371cf7 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -31,7 +31,7 @@ val declare_instance_constant :
   ?hook:(Globnames.global_reference -> unit) ->
   Id.t -> (** name *)
   Id.t Loc.located list option ->
-  bool -> (* polymorphic *)
+  polymorphic:bool ->
   Evd.evar_map -> (* Universes *)
   Constr.t -> (** body *)
   Term.types -> (** type *)
@@ -41,7 +41,7 @@ val new_instance :
   ?abstract:bool -> (** Not abstract by default. *)
   ?global:bool -> (** Not global by default. *)
   ?refine:bool -> (** Allow refinement *)
-  Decl_kinds.polymorphic ->
+  polymorphic:bool ->
   local_binder list ->
   typeclass_constraint ->
   (bool * constr_expr) option ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index caa20b534..40c65b56f 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -90,7 +90,7 @@ let warn_implicits_in_term =
           strbrk "Implicit arguments declaration relies on type." ++ spc () ++
             strbrk "The term declares more implicits than the type here.")
         
-let interp_definition pl bl p red_option c ctypopt =
+let interp_definition pl bl ~polymorphic red_option c ctypopt =
   let env = Global.env() in
   let ctx = Evd.make_evar_universe_context env pl in
   let evdref = ref (Evd.from_ctx ctx) in
@@ -109,7 +109,7 @@ let interp_definition pl bl p red_option c ctypopt =
 	let evd = Evd.restrict_universe_context !evdref vars in
 	let pl, uctx = Evd.universe_context ?names:pl evd in
  	imps1@(Impargs.lift_implicits nb_args imps2), pl,
-	  definition_entry ~univs:uctx ~poly:p body
+	  definition_entry ~univs:uctx ~polymorphic body
     | Some ctyp ->
 	let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
 	let subst = evd_comb0 Evd.nf_univ_variables evdref in
@@ -133,7 +133,7 @@ let interp_definition pl bl p red_option c ctypopt =
         let ctx = Evd.restrict_universe_context !evdref vars in
 	let pl, uctx = Evd.universe_context ?names:pl ctx in
 	imps1@(Impargs.lift_implicits nb_args impsty), pl,
-	  definition_entry ~types:typ ~poly:p 
+	  definition_entry ~types:typ ~polymorphic 
 	    ~univs:uctx body
   in
   red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, pl, imps
@@ -174,7 +174,8 @@ let warn_definition_not_visible =
           strbrk "Section definition " ++
             pr_id ident ++ strbrk " is not visible from current goals")
 
-let declare_definition ident (local, p, k) ce pl imps hook =
+let declare_definition ident def_kind ce pl imps hook =
+  let { locality = local; object_kind = k; _ } = def_kind in
   let fix_exn = Future.fix_exn_of ce.const_entry_body in
   let () = !declare_definition_hook ce in
   let r = match local with
@@ -197,7 +198,7 @@ let _ = Obligations.declare_definition_ref :=
 
 let do_definition ident k pl bl red_option c ctypopt hook =
   let (ce, evd, pl', imps as def) =
-    interp_definition pl bl (pi2 k) red_option c ctypopt
+    interp_definition pl bl k.polymorphic red_option c ctypopt
   in
     if Flags.is_program_mode () then
       let env = Global.env () in
@@ -223,43 +224,48 @@ let do_definition ident k pl bl red_option c ctypopt hook =
 
 (* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
 
-let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl (_,ident) =
-match local with
-| Discharge when Lib.sections_are_opened () ->
-  let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in
-  let _ = declare_variable ident decl in
-  let () = assumption_message ident in
-  let () =
-    if is_verbose () && Pfedit.refining () then
-    Feedback.msg_info (str"Variable" ++ spc () ++ pr_id ident ++
-    strbrk " is not visible from current goals")
-  in
-  let r = VarRef ident in
-  let () = Typeclasses.declare_instance None true r in
-  let () = if is_coe then Class.try_add_new_coercion r ~local:true false in
-  (r,Univ.Instance.empty,true)
-
-| Global | Local | Discharge ->
-  let local = get_locality ident local in
-  let inl = match nl with
-    | NoInline -> None
-    | DefaultInline -> Some (Flags.get_inline_level())
-    | InlineAt i -> Some i
-  in
-  let ctx = Univ.ContextSet.to_context ctx in
-  let decl = (ParameterEntry (None,p,(c,ctx),inl), IsAssumption kind) in
-  let kn = declare_constant ident ~local decl in
-  let gr = ConstRef kn in
-  let () = maybe_declare_manual_implicits false gr imps in
-  let () = Universes.register_universe_binders gr pl in
-  let () = assumption_message ident in
-  let () = Typeclasses.declare_instance None false gr in
-  let () = if is_coe then Class.try_add_new_coercion gr local p in
-  let inst = 
-    if p (* polymorphic *) then Univ.UContext.instance ctx 
-    else Univ.Instance.empty
-  in
-    (gr,inst,Lib.is_modtype_strict ())
+let declare_assumption is_coe assumption_kind (c,ctx) pl imps impl nl (_,ident) =
+  let { locality = local; polymorphic; object_kind = kind } = assumption_kind in
+  match local with
+  | Discharge when Lib.sections_are_opened () ->
+     let entry = SectionLocalAssum { type_context = (c,ctx);
+                                     polymorphic;
+                                     binding_kind = impl }
+     in
+     let decl = (Lib.cwd(), entry, IsAssumption kind) in
+     let _ = declare_variable ident decl in
+     let () = assumption_message ident in
+     let () =
+       if is_verbose () && Pfedit.refining () then
+         Feedback.msg_info (str"Variable" ++ spc () ++ pr_id ident ++
+                              strbrk " is not visible from current goals")
+     in
+     let r = VarRef ident in
+     let () = Typeclasses.declare_instance None true r in
+     let () = if is_coe then Class.try_add_new_coercion r ~local:true false in
+     (r,Univ.Instance.empty,true)
+
+  | Global | Local | Discharge ->
+     let local = get_locality ident local in
+     let inl = match nl with
+       | NoInline -> None
+       | DefaultInline -> Some (Flags.get_inline_level())
+       | InlineAt i -> Some i
+     in
+     let ctx = Univ.ContextSet.to_context ctx in
+     let decl = (ParameterEntry (None,polymorphic,(c,ctx),inl), IsAssumption kind) in
+     let kn = declare_constant ident ~local decl in
+     let gr = ConstRef kn in
+     let () = maybe_declare_manual_implicits false gr imps in
+     let () = Universes.register_universe_binders gr pl in
+     let () = assumption_message ident in
+     let () = Typeclasses.declare_instance None false gr in
+     let () = if is_coe then Class.try_add_new_coercion gr ~local polymorphic in
+     let inst = 
+       if polymorphic then Univ.UContext.instance ctx 
+       else Univ.Instance.empty
+     in
+     (gr,inst,Lib.is_modtype_strict ())
 
 let interp_assumption evdref env impls bl c =
   let c = prod_constr_expr c bl in
@@ -278,12 +284,12 @@ let declare_assumptions idl is_coe k (c,ctx) pl imps impl_is_on nl =
   in
   List.rev refs, status
 
-let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
+let do_assumptions_unbound_univs kind nl l =
   let open Context.Named.Declaration in
   let env = Global.env () in
   let evdref = ref (Evd.from_env env) in
   let l = 
-    if poly then
+    if kind.polymorphic then
       (* Separate declarations so that A B : Type puts A and B in different levels. *)
       List.fold_right (fun (is_coe,(idl,c)) acc ->
         List.fold_right (fun id acc -> 
@@ -305,7 +311,7 @@ let do_assumptions_unbound_univs (_, poly, _ as kind) nl l =
   let l = List.map (on_pi2 (nf_evar evd)) l in
   snd (List.fold_left (fun (subst,status) ((is_coe,idl),t,(ctx,imps)) ->
     let t = replace_vars subst t in
-    let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps false nl in
+    let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps Explicit nl in
     let subst' = List.map2 
       (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u)))
       idl refs 
@@ -323,13 +329,13 @@ let do_assumptions_bound_univs coe kind nl id pl c =
   let evd = Evd.restrict_universe_context !evdref vars in
   let pl, uctx = Evd.universe_context ?names:pl evd in
   let uctx = Univ.ContextSet.of_context uctx in
-  let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls false nl id in
+  let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls Explicit nl id in
   st
 
 let do_assumptions kind nl l = match l with
 | [coe, ([id, Some pl], c)] ->
-  let () = match kind with
-  | (Discharge, _, _) when Lib.sections_are_opened () ->
+  let () = match kind.locality with
+  | Discharge when Lib.sections_are_opened () ->
     let loc = fst id in
     let msg = Pp.str "Section variables cannot be polymorphic." in
     user_err ~loc  msg
@@ -852,8 +858,11 @@ let interp_fix_body env_rec evdref impls (_,ctx) fix ccl =
 
 let build_fix_type (_,ctx) ccl = it_mkProd_or_LetIn ccl ctx
 
-let declare_fix ?(opaque = false) (_,poly,_ as kind) pl ctx f ((def,_),eff) t imps =
-  let ce = definition_entry ~opaque ~types:t ~poly ~univs:ctx ~eff def in
+let declare_fix ?(opaque = false) kind pl ctx f ((def,_),eff) t imps =
+  let polymorphic = kind.polymorphic in
+  let ce =
+    definition_entry ~opaque ~types:t ~polymorphic ~univs:ctx ~eff def
+  in
   declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))
 
 let _ = Obligations.declare_fix_ref :=
@@ -937,7 +946,7 @@ let rec telescope = function
 let nf_evar_context sigma ctx =
   List.map (map_constr (Evarutil.nf_evar sigma)) ctx
 
-let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
+let build_wellfounded (recname,pl,n,bl,arityc,body) polymorphic r measure notation =
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
   let env = Global.env() in
   let ctx = Evd.make_evar_universe_context env pl in
@@ -1048,7 +1057,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
 	let ty = it_mkProd_or_LetIn top_arity binders_rel in
 	let pl, univs = Evd.universe_context ?names:pl !evdref in
 	  (*FIXME poly? *)
-	let ce = definition_entry ~poly ~types:ty ~univs (Evarutil.nf_evar !evdref body) in
+	let ce = definition_entry ~polymorphic ~types:ty ~univs (Evarutil.nf_evar !evdref body) in
 	(** FIXME: include locality *)
 	let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
 	let gr = ConstRef c in
@@ -1170,7 +1179,11 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
       Option.map (List.map Proofview.V82.tactic) init_tac
     in
     let evd = Evd.from_ctx ctx in
-    Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint)
+    let goal_kind = { locality = Global;
+                     polymorphic = poly;
+                     object_kind = DefinitionBody Fixpoint }
+    in
+    Lemmas.start_proof_with_initialization goal_kind
       evd (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
   else begin
     (* We shortcut the proof process *)
@@ -1186,7 +1199,11 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) ind
     let evd = Evd.restrict_universe_context evd vars in
     let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in
     let pl, ctx = Evd.universe_context ?names:pl evd in
-    ignore (List.map4 (declare_fix (local, poly, Fixpoint) pl ctx)
+    let def_kind = { locality = local;
+                     polymorphic = poly;
+                     object_kind = Fixpoint }
+    in
+    ignore (List.map4 (declare_fix def_kind pl ctx)
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     fixpoint_message (Some indexes) fixnames;
@@ -1207,7 +1224,11 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
       Option.map (List.map Proofview.V82.tactic) init_tac
     in
     let evd = Evd.from_ctx ctx in
-      Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
+    let goal_kind = { locality = local;
+                     polymorphic = poly;
+                     object_kind = DefinitionBody CoFixpoint }
+    in
+      Lemmas.start_proof_with_initialization goal_kind
       evd (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
   else begin
     (* We shortcut the proof process *)
@@ -1220,7 +1241,11 @@ let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),pl,ctx,fiximps) n
     let evd = Evd.from_ctx ctx in
     let evd = Evd.restrict_universe_context evd vars in
     let pl, ctx = Evd.universe_context ?names:pl evd in
-    ignore (List.map4 (declare_fix (local, poly, CoFixpoint) pl ctx) 
+    let def_kind = { locality = local;
+                     polymorphic = poly;
+                     object_kind = CoFixpoint }
+    in
+    ignore (List.map4 (declare_fix def_kind pl ctx) 
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     cofixpoint_message fixnames
@@ -1300,9 +1325,13 @@ let do_program_recursive local p fixkind fixl ntns =
         fixl
   end in
   let ctx = Evd.evar_universe_context evd in
-  let kind = match fixkind with
-  | Obligations.IsFixpoint _ -> (local, p, Fixpoint)
-  | Obligations.IsCoFixpoint -> (local, p, CoFixpoint)
+  let object_kind = match fixkind with
+    | Obligations.IsFixpoint _ -> Fixpoint
+    | Obligations.IsCoFixpoint -> CoFixpoint
+  in
+  let kind = { locality = local;
+               polymorphic = p;
+               object_kind }
   in
   Obligations.add_mutual_definitions defs ~kind ?pl ctx ntns fixkind
 
diff --git a/toplevel/command.mli b/toplevel/command.mli
index d35372429..2ae4cddd0 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -32,7 +32,7 @@ val get_declare_definition_hook : unit -> (Safe_typing.private_constants definit
 (** {6 Definitions/Let} *)
 
 val interp_definition :
-  lident list option -> local_binder list -> polymorphic -> red_expr option -> constr_expr ->
+  lident list option -> local_binder list -> polymorphic:bool -> red_expr option -> constr_expr ->
   constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * 
       Universes.universe_binders * Impargs.manual_implicits
 
@@ -55,10 +55,10 @@ val do_definition : Id.t -> definition_kind -> lident list option ->
 val declare_assumption : coercion_flag -> assumption_kind -> 
   types Univ.in_universe_context_set ->
   Universes.universe_binders -> Impargs.manual_implicits ->
-  bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located ->
+  binding_kind -> Vernacexpr.inline -> variable Loc.located ->
   global_reference * Univ.Instance.t * bool
 
-val do_assumptions : locality * polymorphic * assumption_object_kind ->
+val do_assumptions : assumption_kind ->
   Vernacexpr.inline -> (plident list * constr_expr) with_coercion list -> bool
 
 (* val declare_assumptions : variable Loc.located list -> *)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index aa1a489c2..ceef929b9 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -490,7 +490,7 @@ let declare_definition prg =
     Evd.universe_context ?names:prg.prg_pl (Evd.from_ctx prg.prg_ctx) in
   let ce =
     definition_entry ~fix_exn
-     ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
+     ~opaque ~types:(nf typ) ~polymorphic:prg.prg_kind.polymorphic
      ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body)
   in
   let () = progmap_remove prg in
@@ -542,7 +542,6 @@ let declare_mutual_definition l =
   let fixkind = Option.get first.prg_fixkind in
   let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
   let fixdecls = (Array.of_list (List.map (fun x -> Name x.prg_name) l), arrrec, recvec) in
-  let (local,poly,kind) = first.prg_kind in
   let fixnames = first.prg_deps in
   let opaque = first.prg_opaque in
   let kind = if fixkind != IsCoFixpoint then Fixpoint else CoFixpoint in
@@ -567,14 +566,16 @@ let declare_mutual_definition l =
   (* Declare the recursive definitions *)
   let ctx = Evd.evar_context_universe_context first.prg_ctx in
   let fix_exn = Stm.get_fix_exn () in
-  let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, kind) ctx)
+  let def_kind = { first.prg_kind with object_kind = kind } in
+  let kns = List.map4 (!declare_fix_ref ~opaque def_kind ctx)
     fixnames fixdecls fixtypes fiximps in
     (* Declare notations *)
     List.iter Metasyntax.add_notation_interpretation first.prg_notations;
     Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
     let gr = List.hd kns in
     let kn = match gr with ConstRef kn -> kn | _ -> assert false in
-    Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx;
+    Lemmas.call_hook fix_exn first.prg_hook first.prg_kind.locality gr
+                     first.prg_ctx;
     List.iter progmap_remove l; kn
 
 let decompose_lam_prod c ty =
@@ -633,7 +634,7 @@ let declare_obligation prg obl body ty uctx =
   | _, Evar_kinds.Expand -> false, { obl with obl_body = Some (TermObl body) }
   | force, Evar_kinds.Define opaque ->
       let opaque = not force && opaque in
-      let poly = pi2 prg.prg_kind in
+      let poly = prg.prg_kind.polymorphic in
       let ctx, body, ty, args =
 	if get_shrink_obligations () && not poly then
 	  shrink_body body ty else [], body, ty, [||]
@@ -791,9 +792,15 @@ let dependencies obls n =
       obls;
     !res
 
-let goal_kind poly = Decl_kinds.Local, poly, Decl_kinds.DefinitionBody Decl_kinds.Definition
+let goal_kind ~polymorphic =
+  { locality = Decl_kinds.Local;
+    polymorphic;
+    object_kind =  Decl_kinds.DefinitionBody Decl_kinds.Definition }
 
-let goal_proof_kind poly = Decl_kinds.Local, poly, Decl_kinds.Proof Decl_kinds.Lemma
+let goal_proof_kind ~polymorphic =
+  { locality = Decl_kinds.Local;
+    polymorphic;
+    object_kind = Decl_kinds.Proof Decl_kinds.Lemma }
 
 let kind_of_obligation poly o =
   match o with
@@ -891,7 +898,7 @@ in
   let _ = obls.(num) <- obl in
   let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in
   let ctx' =
-    if not (pi2 prg.prg_kind) (* Not polymorphic *) then
+    if not prg.prg_kind.polymorphic then
       (* The universe context was declared globally, we continue
          from the new global environment. *)
       let evd = Evd.from_env (Global.env ()) in
@@ -925,7 +932,7 @@ let rec solve_obligation prg num tac =
         ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) remaining));
   in
   let obl = subst_deps_obl obls obl in
-  let kind = kind_of_obligation (pi2 prg.prg_kind) (snd obl.obl_status) in
+  let kind = kind_of_obligation prg.prg_kind.polymorphic (snd obl.obl_status) in
   let evd = Evd.from_ctx prg.prg_ctx in
   let evd = Evd.update_sigma_env evd (Global.env ()) in
   let auto n tac oblset = auto_solve_obligations n ~oblset tac in
@@ -969,13 +976,13 @@ and solve_obligation_by_tac prg obls i tac =
 	    let evd = Evd.update_sigma_env evd (Global.env ()) in
 	    let t, ty, ctx =
 	      solve_by_tac obl.obl_name (evar_of_obligation obl) tac
-	        (pi2 prg.prg_kind) (Evd.evar_universe_context evd)
+	        prg.prg_kind.polymorphic (Evd.evar_universe_context evd)
 	    in
 	    let uctx = Evd.evar_context_universe_context ctx in
 	    let prg = {prg with prg_ctx = ctx} in
 	    let def, obl' = declare_obligation prg obl t ty uctx in
 	      obls.(i) <- obl';
-	      if def && not (pi2 prg.prg_kind) then (
+	      if def && not (prg.prg_kind.polymorphic) then (
 	        (* Declare the term constraints with the first obligation only *)
 	        let evd = Evd.from_env (Global.env ()) in
 	        let evd = Evd.merge_universe_subst evd (Evd.universe_subst (Evd.from_ctx ctx)) in
@@ -1071,7 +1078,12 @@ let show_term n =
 	     Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
 	    ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body)
 
-let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
+let default_definition_kind =
+  { locality = Global;
+    polymorphic = false;
+    object_kind = Definition }
+
+let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=default_definition_kind) ?tactic
     ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
   let sign = Decls.initialize_named_context_for_proof () in
   let info = Id.print n ++ str " has type-checked" in
@@ -1090,7 +1102,7 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definit
 	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
 	| _ -> res)
 
-let add_mutual_definitions l ctx ?pl ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
+let add_mutual_definitions l ctx ?pl ?tactic ?(kind=default_definition_kind) ?(reduce=reduce)
     ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
   let sign = Decls.initialize_named_context_for_proof () in
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index de056fa9b..c98599d7f 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -426,7 +426,7 @@ let implicits_of_context ctx =
     in ExplByPos (i, explname), (true, true, true))
     1 (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
 
-let declare_class finite def poly ctx id idbuild paramimpls params arity 
+let declare_class finite def ~polymorphic ctx id idbuild paramimpls params arity 
     template fieldimpls fields ?(kind=StructureComponent) is_coe coers priorities sign =
   let fieldimpls =
     (* Make the class implicit in the projections, and the params if applicable. *)
@@ -441,11 +441,11 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity
       let class_body = it_mkLambda_or_LetIn field params in
       let class_type = it_mkProd_or_LetIn arity params in
       let class_entry = 
-	Declare.definition_entry ~types:class_type ~poly ~univs:ctx class_body in
+	Declare.definition_entry ~types:class_type ~polymorphic ~univs:ctx class_body in
       let cst = Declare.declare_constant (snd id)
 	(DefinitionEntry class_entry, IsDefinition Definition)
       in
-      let cstu = (cst, if poly then Univ.UContext.instance ctx else Univ.Instance.empty) in
+      let cstu = (cst, if polymorphic then Univ.UContext.instance ctx else Univ.Instance.empty) in
       let inst_type = appvectc (mkConstU cstu)
 			       (Termops.rel_vect 0 (List.length params)) in
       let proj_type =
@@ -453,8 +453,8 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity
       let proj_body =
 	it_mkLambda_or_LetIn (mkLambda (Name binder_name, inst_type, mkRel 1)) params in
       let proj_entry =
-	Declare.definition_entry ~types:proj_type ~poly
-	    ~univs:(if poly then ctx else Univ.UContext.empty) proj_body
+	Declare.definition_entry ~types:proj_type ~polymorphic
+	    ~univs:(if polymorphic then ctx else Univ.UContext.empty) proj_body
       in
       let proj_cst = Declare.declare_constant proj_name
         (DefinitionEntry proj_entry, IsDefinition Definition)
@@ -469,7 +469,7 @@ let declare_class finite def poly ctx id idbuild paramimpls params arity
       in
       cref, [Name proj_name, sub, Some proj_cst]
     | _ ->
-       let ind = declare_structure BiFinite poly ctx (snd id) idbuild paramimpls
+       let ind = declare_structure BiFinite polymorphic ctx (snd id) idbuild paramimpls
 	  params arity template fieldimpls fields
 	  ~kind:Method ~name:binder_name false (List.map (fun _ -> false) fields) sign
        in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 14d9a55c6..b8d44f32b 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -469,15 +469,22 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
   in
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
-	  start_proof_and_print (local,p,DefinitionBody k)
-	    [Some (lid,pl), (bl,t,None)] hook
+       let goal_kind = { locality = local;
+                         polymorphic = p;
+                         object_kind = DefinitionBody k }
+       in
+       start_proof_and_print goal_kind [Some (lid,pl), (bl,t,None)] hook
     | DefineBody (bl,red_option,c,typ_opt) ->
  	let red_option = match red_option with
           | None -> None
           | Some r ->
-	      let (evc,env)= get_current_context () in
- 		Some (snd (Hook.get f_interp_redexp env evc r)) in
-	do_definition id (local,p,k) pl bl red_option c typ_opt hook)
+             let (evc,env)= get_current_context () in
+             Some (snd (Hook.get f_interp_redexp env evc r)) in
+        let def_kind = { locality = local;
+                         polymorphic = p;
+                         object_kind = k }
+        in
+        do_definition id def_kind pl bl red_option c typ_opt hook)
 
 let vernac_start_proof locality p kind l lettop =
   let local = enforce_locality_exp locality None in
@@ -490,7 +497,11 @@ let vernac_start_proof locality p kind l lettop =
     if lettop then
       user_err ~hdr:"Vernacentries.StartProof"
 	(str "Let declarations can only be used in proof editing mode.");
-  start_proof_and_print (local, p, Proof kind) l no_hook
+  let goal_kind = { locality = local;
+                    polymorphic = p;
+                    object_kind = Proof kind }
+  in
+  start_proof_and_print goal_kind l no_hook
 
 let qed_display_script = ref true
 
@@ -514,7 +525,10 @@ let vernac_exact_proof c =
 let vernac_assumption locality poly (local, kind) l nl =
   let local = enforce_locality_exp locality local in
   let global = local == Global in
-  let kind = local, poly, kind in
+  let kind = {locality = local;
+              polymorphic = poly;
+              object_kind = kind }
+  in
   List.iter (fun (is_coe,(idl,c)) ->
     if Dumpglob.dump () then
       List.iter (fun (lid, _) ->
@@ -814,10 +828,10 @@ let vernac_identity_coercion locality poly local id qids qidt =
 
 (* Type classes *)
 
-let vernac_instance abst locality poly sup inst props pri =
+let vernac_instance abst locality ~polymorphic sup inst props pri =
   let global = not (make_section_locality locality) in
   Dumpglob.dump_constraint inst false "inst";
-  ignore(Classes.new_instance ~abstract:abst ~global poly sup inst props pri)
+  ignore(Classes.new_instance ~abstract:abst ~global ~polymorphic sup inst props pri)
 
 let vernac_context poly l =
   if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom