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

Was PR#283: Stylistic improvements in intf/decl_kinds.mli.

8 files changed, 169 insertions, 104 deletions

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 0dc7990143..9582015a08 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 ad4a13c218..a0a8d2aaf0 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 7beb873e63..fc7371cf78 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 caa20b534a..7bb016d34a 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;
+                                     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 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 d353724294..f0651a98c8 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 ->
+  implicit_status -> 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 aa1a489c22..ceef929b90 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 de056fa9b2..c98599d7f2 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 aa1999cf1e..e9fb8bd66f 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