Revert "Merge remote-tracking branch 'github/pr/283' into trunk"

I hadn't realized that this PR uses OCaml's 4.03 inlined records
feature. I will advocate again for a switch to the latest OCaml stable
version, but meanwhile, let's revert. Sorry for the noise.

This reverts commit 3c47248abc27aa9c64120db30dcb0d7bf945bc70, reversing
changes made to ceb68d1d643ac65f500e0201f61e73cf22e6e2fb.

8 files changed, 104 insertions, 169 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 9582015a08..0dc7990143 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 ~polymorphic =
+let build_id_coercion idf_opt source poly =
   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 ~polymorphic =
   in
   let constr_entry = (* Cast is necessary to express [val_f] is identity *)
     DefinitionEntry
-      (definition_entry ~types:typ_f ~polymorphic ~univs:(snd (Evd.universe_context sigma))
+      (definition_entry ~types:typ_f ~poly ~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 a0a8d2aaf0..ad4a13c218 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 ~polymorphic evm term termtype =
+let declare_instance_constant k pri global imps ?hook id pl poly 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 ~polymorphic evm ter
   in
   let pl, uctx = Evd.universe_context ?names:pl evm in
   let entry = 
-    Declare.definition_entry ~types:termtype ~polymorphic ~univs:uctx term
+    Declare.definition_entry ~types:termtype ~poly ~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 ~polymorphic evm ter
     instance_hook k pri global imps ?hook (ConstRef kn);
     id
 
-let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~polymorphic ctx (instid, bk, cl) props
+let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) poly 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) ~
 	let pl, ctx = Evd.universe_context ?names:pl !evars in
 	let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
 	  (ParameterEntry 
-            (None,polymorphic,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
+            (None,poly,(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,12 +294,9 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~
       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
-            ~polymorphic evm (Option.get term) termtype
+            poly evm (Option.get term) termtype
 	else if Flags.is_program_mode () || refine || Option.is_empty term then begin
-            let kind = { locality = Decl_kinds.Global;
-                         polymorphic;
-                         object_kind = Decl_kinds.DefinitionBody Decl_kinds.Instance }
-            in
+	  let kind = Decl_kinds.Global, poly, 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
@@ -316,12 +313,8 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~
 	      in
               let hook = Lemmas.mk_hook hook in
 	      let ctx = Evd.evar_universe_context evm in
-              let kind = { locality = Global;
-                           polymorphic;
-                           object_kind = Instance }
-              in
-                ignore (Obligations.add_definition id ?term:constr
- 			?pl typ ctx ~kind ~hook obls);
+		ignore (Obligations.add_definition id ?term:constr
+ 			?pl typ ctx ~kind:(Global,poly,Instance) ~hook obls);
 		id
 	    else
 	      (Flags.silently 
@@ -397,11 +390,8 @@ let context poly l =
       | ExplByPos (_, Some id') -> Id.equal id id'
       | _ -> false
       in
-      let impl = if List.exists test impls then Implicit else Explicit in
-      let decl = { locality = Discharge;
-                   polymorphic = poly;
-                   object_kind = Definitional }
-      in
+      let impl = List.exists test impls in
+      let decl = (Discharge, poly, 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 fc7371cf78..7beb873e63 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 ->
-  polymorphic:bool ->
+  bool -> (* polymorphic *)
   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 *)
-  polymorphic:bool ->
+  Decl_kinds.polymorphic ->
   local_binder list ->
   typeclass_constraint ->
   (bool * constr_expr) option ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7bb016d34a..caa20b534a 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 ~polymorphic red_option c ctypopt =
+let interp_definition pl bl p 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 ~polymorphic 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 ~polymorphic body
+	  definition_entry ~univs:uctx ~poly:p 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 ~polymorphic 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 ~polymorphic 
+	  definition_entry ~types:typ ~poly:p 
 	    ~univs:uctx body
   in
   red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, pl, imps
@@ -174,8 +174,7 @@ let warn_definition_not_visible =
           strbrk "Section definition " ++
             pr_id ident ++ strbrk " is not visible from current goals")
 
-let declare_definition ident def_kind ce pl imps hook =
-  let { locality = local; object_kind = k; _ } = def_kind in
+let declare_definition ident (local, p, k) ce pl imps hook =
   let fix_exn = Future.fix_exn_of ce.const_entry_body in
   let () = !declare_definition_hook ce in
   let r = match local with
@@ -198,7 +197,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 k.polymorphic red_option c ctypopt
+    interp_definition pl bl (pi2 k) red_option c ctypopt
   in
     if Flags.is_program_mode () then
       let env = Global.env () in
@@ -224,48 +223,43 @@ let do_definition ident k pl bl red_option c ctypopt hook =
 
 (* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
 
-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;
-                                     implicit_status = 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 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 interp_assumption evdref env impls bl c =
   let c = prod_constr_expr c bl in
@@ -284,12 +278,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 kind nl l =
+let do_assumptions_unbound_univs (_, poly, _ as 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 kind.polymorphic then
+    if poly 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 -> 
@@ -311,7 +305,7 @@ let do_assumptions_unbound_univs 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 Explicit nl in
+    let (refs,status') = declare_assumptions idl is_coe kind (t,ctx) [] imps false nl in
     let subst' = List.map2 
       (fun (_,id) (c,u) -> (id,Universes.constr_of_global_univ (c,u)))
       idl refs 
@@ -329,13 +323,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 Explicit nl id in
+  let (_, _, st) = declare_assumption coe kind (ty, uctx) pl impls false nl id in
   st
 
 let do_assumptions kind nl l = match l with
 | [coe, ([id, Some pl], c)] ->
-  let () = match kind.locality with
-  | Discharge when Lib.sections_are_opened () ->
+  let () = match kind 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
@@ -858,11 +852,8 @@ 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) 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
+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
   declare_definition f kind ce pl imps (Lemmas.mk_hook (fun _ r -> r))
 
 let _ = Obligations.declare_fix_ref :=
@@ -946,7 +937,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) polymorphic r measure notation =
+let build_wellfounded (recname,pl,n,bl,arityc,body) poly 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
@@ -1057,7 +1048,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) polymorphic r measure notati
 	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 ~polymorphic ~types:ty ~univs (Evarutil.nf_evar !evdref body) in
+	let ce = definition_entry ~poly ~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
@@ -1179,11 +1170,7 @@ 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
-    let goal_kind = { locality = Global;
-                     polymorphic = poly;
-                     object_kind = DefinitionBody Fixpoint }
-    in
-    Lemmas.start_proof_with_initialization goal_kind
+    Lemmas.start_proof_with_initialization (Global,poly,DefinitionBody Fixpoint)
       evd (Some(false,indexes,init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
   else begin
     (* We shortcut the proof process *)
@@ -1199,11 +1186,7 @@ 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
-    let def_kind = { locality = local;
-                     polymorphic = poly;
-                     object_kind = Fixpoint }
-    in
-    ignore (List.map4 (declare_fix def_kind pl ctx)
+    ignore (List.map4 (declare_fix (local, poly, Fixpoint) pl ctx)
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     fixpoint_message (Some indexes) fixnames;
@@ -1224,11 +1207,7 @@ 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
-    let goal_kind = { locality = local;
-                     polymorphic = poly;
-                     object_kind = DefinitionBody CoFixpoint }
-    in
-      Lemmas.start_proof_with_initialization goal_kind
+      Lemmas.start_proof_with_initialization (Global,poly, DefinitionBody CoFixpoint)
       evd (Some(true,[],init_tac)) thms None (Lemmas.mk_hook (fun _ _ -> ()))
   else begin
     (* We shortcut the proof process *)
@@ -1241,11 +1220,7 @@ 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
-    let def_kind = { locality = local;
-                     polymorphic = poly;
-                     object_kind = CoFixpoint }
-    in
-    ignore (List.map4 (declare_fix def_kind pl ctx) 
+    ignore (List.map4 (declare_fix (local, poly, CoFixpoint) pl ctx) 
 	      fixnames fixdecls fixtypes fiximps);
     (* Declare the recursive definitions *)
     cofixpoint_message fixnames
@@ -1325,13 +1300,9 @@ let do_program_recursive local p fixkind fixl ntns =
         fixl
   end in
   let ctx = Evd.evar_universe_context evd in
-  let object_kind = match fixkind with
-    | Obligations.IsFixpoint _ -> Fixpoint
-    | Obligations.IsCoFixpoint -> CoFixpoint
-  in
-  let kind = { locality = local;
-               polymorphic = p;
-               object_kind }
+  let kind = match fixkind with
+  | Obligations.IsFixpoint _ -> (local, p, Fixpoint)
+  | Obligations.IsCoFixpoint -> (local, p, CoFixpoint)
   in
   Obligations.add_mutual_definitions defs ~kind ?pl ctx ntns fixkind
 
diff --git a/toplevel/command.mli b/toplevel/command.mli
index f0651a98c8..d353724294 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:bool -> red_expr option -> constr_expr ->
+  lident list option -> local_binder list -> polymorphic -> 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 ->
-  implicit_status -> Vernacexpr.inline -> variable Loc.located ->
+  bool (** implicit *) -> Vernacexpr.inline -> variable Loc.located ->
   global_reference * Univ.Instance.t * bool
 
-val do_assumptions : assumption_kind ->
+val do_assumptions : locality * polymorphic * assumption_object_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 ceef929b90..aa1a489c22 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) ~polymorphic:prg.prg_kind.polymorphic
+     ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
      ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body)
   in
   let () = progmap_remove prg in
@@ -542,6 +542,7 @@ 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
@@ -566,16 +567,14 @@ 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 def_kind = { first.prg_kind with object_kind = kind } in
-  let kns = List.map4 (!declare_fix_ref ~opaque def_kind ctx)
+  let kns = List.map4 (!declare_fix_ref ~opaque (local, poly, 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 first.prg_kind.locality gr
-                     first.prg_ctx;
+    Lemmas.call_hook fix_exn first.prg_hook local gr first.prg_ctx;
     List.iter progmap_remove l; kn
 
 let decompose_lam_prod c ty =
@@ -634,7 +633,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 = prg.prg_kind.polymorphic in
+      let poly = pi2 prg.prg_kind in
       let ctx, body, ty, args =
 	if get_shrink_obligations () && not poly then
 	  shrink_body body ty else [], body, ty, [||]
@@ -792,15 +791,9 @@ let dependencies obls n =
       obls;
     !res
 
-let goal_kind ~polymorphic =
-  { locality = Decl_kinds.Local;
-    polymorphic;
-    object_kind =  Decl_kinds.DefinitionBody Decl_kinds.Definition }
+let goal_kind poly = Decl_kinds.Local, poly, Decl_kinds.DefinitionBody Decl_kinds.Definition
 
-let goal_proof_kind ~polymorphic =
-  { locality = Decl_kinds.Local;
-    polymorphic;
-    object_kind = Decl_kinds.Proof Decl_kinds.Lemma }
+let goal_proof_kind poly = Decl_kinds.Local, poly, Decl_kinds.Proof Decl_kinds.Lemma
 
 let kind_of_obligation poly o =
   match o with
@@ -898,7 +891,7 @@ in
   let _ = obls.(num) <- obl in
   let ctx' = match ctx' with None -> prg.prg_ctx | Some ctx' -> ctx' in
   let ctx' =
-    if not prg.prg_kind.polymorphic then
+    if not (pi2 prg.prg_kind) (* Not polymorphic *) then
       (* The universe context was declared globally, we continue
          from the new global environment. *)
       let evd = Evd.from_env (Global.env ()) in
@@ -932,7 +925,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 prg.prg_kind.polymorphic (snd obl.obl_status) in
+  let kind = kind_of_obligation (pi2 prg.prg_kind) (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
@@ -976,13 +969,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
-	        prg.prg_kind.polymorphic (Evd.evar_universe_context evd)
+	        (pi2 prg.prg_kind) (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 (prg.prg_kind.polymorphic) then (
+	      if def && not (pi2 prg.prg_kind) 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
@@ -1078,12 +1071,7 @@ 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 default_definition_kind =
-  { locality = Global;
-    polymorphic = false;
-    object_kind = Definition }
-
-let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=default_definition_kind) ?tactic
+let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definition) ?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
@@ -1102,7 +1090,7 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=default_definition_k
 	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
 	| _ -> res)
 
-let add_mutual_definitions l ctx ?pl ?tactic ?(kind=default_definition_kind) ?(reduce=reduce)
+let add_mutual_definitions l ctx ?pl ?tactic ?(kind=Global,false,Definition) ?(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 c98599d7f2..de056fa9b2 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 ~polymorphic ctx id idbuild paramimpls params arity 
+let declare_class finite def poly 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 ~polymorphic 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 ~polymorphic ~univs:ctx class_body in
+	Declare.definition_entry ~types:class_type ~poly ~univs:ctx class_body in
       let cst = Declare.declare_constant (snd id)
 	(DefinitionEntry class_entry, IsDefinition Definition)
       in
-      let cstu = (cst, if polymorphic then Univ.UContext.instance ctx else Univ.Instance.empty) in
+      let cstu = (cst, if poly 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 ~polymorphic 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 ~polymorphic
-	    ~univs:(if polymorphic then ctx else Univ.UContext.empty) proj_body
+	Declare.definition_entry ~types:proj_type ~poly
+	    ~univs:(if poly 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 ~polymorphic ctx id idbuild paramimpls params arity
       in
       cref, [Name proj_name, sub, Some proj_cst]
     | _ ->
-       let ind = declare_structure BiFinite polymorphic ctx (snd id) idbuild paramimpls
+       let ind = declare_structure BiFinite poly 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 e9fb8bd66f..aa1999cf1e 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -469,22 +469,15 @@ let vernac_definition locality p (local,k) ((loc,id as lid),pl) def =
   in
   (match def with
     | ProveBody (bl,t) ->   (* local binders, typ *)
-       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
+	  start_proof_and_print (local,p,DefinitionBody k)
+	    [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
-        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 (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 vernac_start_proof locality p kind l lettop =
   let local = enforce_locality_exp locality None in
@@ -497,11 +490,7 @@ 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.");
-  let goal_kind = { locality = local;
-                    polymorphic = p;
-                    object_kind = Proof kind }
-  in
-  start_proof_and_print goal_kind l no_hook
+  start_proof_and_print (local, p, Proof kind) l no_hook
 
 let qed_display_script = ref true
 
@@ -525,10 +514,7 @@ 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 = {locality = local;
-              polymorphic = poly;
-              object_kind = kind }
-  in
+  let kind = local, poly, kind in
   List.iter (fun (is_coe,(idl,c)) ->
     if Dumpglob.dump () then
       List.iter (fun (lid, _) ->
@@ -828,10 +814,10 @@ let vernac_identity_coercion locality poly local id qids qidt =
 
 (* Type classes *)
 
-let vernac_instance abst locality ~polymorphic sup inst props pri =
+let vernac_instance abst locality poly 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 ~polymorphic sup inst props pri)
+  ignore(Classes.new_instance ~abstract:abst ~global poly sup inst props pri)
 
 let vernac_context poly l =
   if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom