[lemmas] [proof] Split proof kinds into per-layer components.

We split `{goal,declaration,assumption}_kind` into their
components. This makes sense as each part of this triple is handled by
a different layer, namely:

- `polymorphic` status: necessary for the lower engine layers;
- `locality`: only used in `vernac` top-level constants
- `kind`: merely used for cosmetic purposes [could indeed be removed /
  pushed upwards]

We also profit from this refactoring to add some named parameters to
the top-level definition API which is quite parameter-hungry.

More refactoring is possible and will come in further commits, in
particular this is a step towards unifying the definition / lemma save path.

18 files changed, 225 insertions, 191 deletions

diff --git a/vernac/classes.ml b/vernac/classes.ml
index bb5ebd7148..c8ae9928a3 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -362,9 +362,8 @@ let declare_instance_program env sigma ~global ~poly id pri imps decl term termt
   in
   let hook = DeclareDef.Hook.make hook in
   let ctx = Evd.evar_universe_context sigma in
-  ignore(Obligations.add_definition id ?term:constr
-           ~univdecl:decl typ ctx ~kind:(Global ImportDefaultBehavior,poly,Instance) ~hook obls)
-
+  ignore(Obligations.add_definition ~name:id ?term:constr
+           ~univdecl:decl ~scope:(Global ImportDefaultBehavior) ~poly ~kind:Instance ~hook typ ctx obls)
 
 let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype =
   (* spiwack: it is hard to reorder the actions to do
@@ -373,10 +372,11 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t
      the refinement manually.*)
   let gls = List.rev (Evd.future_goals sigma) in
   let sigma = Evd.reset_future_goals sigma in
-  let kind = Decl_kinds.Global ImportDefaultBehavior, Decl_kinds.DefinitionBody Decl_kinds.Instance in
+  let scope = Decl_kinds.(Global ImportDefaultBehavior) in
+  let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in
   let hook = DeclareDef.Hook.make (fun _ _ _ -> instance_hook pri global imps ?hook) in
-  let info = Lemmas.Info.make ~hook () in
-  let lemma = Lemmas.start_lemma ~name:id ~poly ~kind ~udecl ~info sigma (EConstr.of_constr termtype) in
+  let info = Lemmas.Info.make ~hook ~scope ~kind () in
+  let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info sigma (EConstr.of_constr termtype) in
   (* spiwack: I don't know what to do with the status here. *)
   let lemma =
     if not (Option.is_empty term) then
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index b0297b7c51..febe28879f 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -43,14 +43,14 @@ let should_axiom_into_instance = function
     true
   | Definitional | Logical | Conjectural -> !axiom_into_instance
 
-let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} =
-match local with
+let declare_assumption is_coe ~poly ~scope ~kind (c,ctx) pl imps impl nl {CAst.v=ident} =
+match scope with
 | Discharge ->
   let ctx = match ctx with
     | Monomorphic_entry ctx -> ctx
     | Polymorphic_entry (_, ctx) -> Univ.ContextSet.of_context ctx
   in
-  let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in
+  let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),poly,impl), IsAssumption kind) in
   let _ = declare_variable ident decl in
   let () = assumption_message ident in
   let r = VarRef ident in
@@ -78,7 +78,7 @@ match local with
   let sigma = Evd.from_env env in
   let () = if do_instance then Classes.declare_instance env sigma None false gr in
   let local = match local with ImportNeedQualified -> true | ImportDefaultBehavior -> false in
-  let () = if is_coe then Class.try_add_new_coercion gr ~local p in
+  let () = if is_coe then Class.try_add_new_coercion gr ~local poly in
   let inst = match ctx with
     | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx
     | Monomorphic_entry _ -> Univ.Instance.empty
@@ -96,11 +96,11 @@ let next_uctx =
   | Polymorphic_entry _ as uctx -> uctx
   | Monomorphic_entry _ -> empty_uctx
 
-let declare_assumptions idl is_coe k (c,uctx) pl imps nl =
+let declare_assumptions idl is_coe ~scope ~poly ~kind (c,uctx) pl imps nl =
   let refs, status, _ =
     List.fold_left (fun (refs,status,uctx) id ->
       let ref',u',status' =
-        declare_assumption is_coe k (c,uctx) pl imps false nl id in
+        declare_assumption is_coe ~scope ~poly ~kind (c,uctx) pl imps false nl id in
       (ref',u')::refs, status' && status, next_uctx uctx)
       ([],true,uctx) idl
   in
@@ -115,7 +115,7 @@ let maybe_error_many_udecls = function
           str "(which will be shared by the whole block).")
   | (_, None) -> ()
 
-let process_assumptions_udecls kind l =
+let process_assumptions_udecls ~scope l =
   let udecl, first_id = match l with
     | (coe, ((id, udecl)::rest, c))::rest' ->
       List.iter maybe_error_many_udecls rest;
@@ -123,8 +123,8 @@ let process_assumptions_udecls kind l =
       udecl, id
     | (_, ([], _))::_ | [] -> assert false
   in
-  let () = match kind, udecl with
-    | (Discharge, _, _), Some _ ->
+  let () = match scope, udecl with
+    | Discharge, Some _ ->
       let loc = first_id.CAst.loc in
       let msg = Pp.str "Section variables cannot be polymorphic." in
       user_err ?loc  msg
@@ -132,13 +132,13 @@ let process_assumptions_udecls kind l =
   in
   udecl, List.map (fun (coe, (idl, c)) -> coe, (List.map fst idl, c)) l
 
-let do_assumptions ~program_mode kind nl l =
+let do_assumptions ~program_mode ~poly ~scope ~kind nl l =
   let open Context.Named.Declaration in
   let env = Global.env () in
-  let udecl, l = process_assumptions_udecls kind l in
+  let udecl, l = process_assumptions_udecls ~scope l in
   let sigma, udecl = interp_univ_decl_opt env udecl in
   let l =
-    if pi2 kind (* poly *) 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 ->
@@ -174,11 +174,11 @@ let do_assumptions ~program_mode kind nl l =
      IMO, thus I think we should adapt `prepare_parameter` to handle
      this case too. *)
   let sigma = Evd.restrict_universe_context sigma uvars in
-  let uctx = Evd.check_univ_decl ~poly:(pi2 kind) sigma udecl in
+  let uctx = Evd.check_univ_decl ~poly sigma udecl in
   let ubinders = Evd.universe_binders sigma in
   pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) ->
       let t = replace_vars subst t in
-      let refs, status' = declare_assumptions  idl is_coe kind (t,uctx) ubinders imps nl in
+      let refs, status' = declare_assumptions idl is_coe ~poly ~scope ~kind (t,uctx) ubinders imps nl in
       let subst' = List.map2
           (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u)))
           idl refs
@@ -288,17 +288,15 @@ let context poly l =
       | _ -> false
       in
       let impl = List.exists test impls in
-      let persistence =
+      let scope =
         if Lib.sections_are_opened () then Discharge else Global ImportDefaultBehavior in
-      let decl = (persistence, poly, Context) in
       let nstatus = match b with
       | None ->
-        pi3 (declare_assumption false decl (t, univs) UnivNames.empty_binders [] impl
+        pi3 (declare_assumption false ~scope ~poly ~kind:Context (t, univs) UnivNames.empty_binders [] impl
                Declaremods.NoInline (CAst.make id))
       | Some b ->
-        let decl = (Discharge, poly, Definition) in
         let entry = Declare.definition_entry ~univs ~types:t b in
-        let _gr = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] in
+        let _gr = DeclareDef.declare_definition ~name:id ~scope:Discharge ~kind:Definition UnivNames.empty_binders entry [] in
         Lib.sections_are_opened () || Lib.is_modtype_strict ()
       in
         status && nstatus
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 07e96d87a2..67fa94ceb8 100644
--- a/vernac/comAssumption.mli
+++ b/vernac/comAssumption.mli
@@ -16,8 +16,10 @@ open Decl_kinds
 (** {6 Parameters/Assumptions} *)
 
 val do_assumptions
-  : program_mode:bool
-  -> locality * polymorphic * assumption_object_kind
+  :  program_mode:bool
+  -> poly:polymorphic
+  -> scope:locality
+  -> kind:assumption_object_kind
   -> Declaremods.inline
   -> (ident_decl list * constr_expr) with_coercion list
   -> bool
@@ -26,7 +28,9 @@ val do_assumptions
     nor in a module type and meant to be instantiated. *)
 val declare_assumption
   : coercion_flag
-  -> assumption_kind
+  -> poly:bool
+  -> scope:Decl_kinds.locality
+  -> kind:assumption_object_kind
   -> Constr.types Entries.in_universes_entry
   -> UnivNames.universe_binders
   -> Impargs.manual_implicits
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index b3cc0a4236..3d5ea319bb 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -79,9 +79,9 @@ let check_definition ~program_mode (ce, evd, _, imps) =
   check_evars_are_solved ~program_mode env evd;
   ce
 
-let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
+let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind univdecl bl red_option c ctypopt =
   let (ce, evd, univdecl, imps as def) =
-    interp_definition ~program_mode univdecl bl (pi2 k) red_option c ctypopt
+    interp_definition ~program_mode univdecl bl poly red_option c ctypopt
   in
   if program_mode then
     let env = Global.env () in
@@ -95,13 +95,13 @@ let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt =
       | None -> Retyping.get_type_of env evd c
     in
     let obls, _, c, cty =
-      Obligations.eterm_obligations env ident evd 0 c typ
+      Obligations.eterm_obligations env name evd 0 c typ
     in
     let ctx = Evd.evar_universe_context evd in
     ignore(Obligations.add_definition
-             ident ~term:c cty ctx ~univdecl ~implicits:imps ~kind:k ?hook obls)
+             ~name ~term:c cty ctx ~univdecl ~implicits:imps ~scope ~poly ~kind ?hook obls)
   else
     let ce = check_definition ~program_mode def in
     let uctx = Evd.evar_universe_context evd in
     let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
-    ignore(DeclareDef.declare_definition ident k ?hook_data ce (Evd.universe_binders evd) imps)
+    ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data (Evd.universe_binders evd) ce imps)
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 256abed6a1..ec59916e3c 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -16,10 +16,12 @@ open Constrexpr
 (** {6 Definitions/Let} *)
 
 val do_definition
-  : program_mode:bool
+  :  program_mode:bool
   -> ?hook:DeclareDef.Hook.t
-  -> Id.t
-  -> definition_kind
+  -> name:Id.t
+  -> scope:locality
+  -> poly:bool
+  -> kind:definition_object_kind
   -> universe_decl_expr option
   -> local_binder_expr list
   -> red_expr option
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 6d9aa746b9..e3428d6afc 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -255,7 +255,7 @@ let interp_fixpoint ~cofix l ntns =
   let uctx,fix = ground_fixpoint env evd fix in
   (fix,pl,uctx,info)
 
-let declare_fixpoint_interactive_generic ?indexes local poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns =
+let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs,fixdefs,fixtypes),udecl,ctx,fiximps) ntns =
   let fix_kind, cofix, indexes = match indexes with
     | Some indexes -> Fixpoint, false, indexes
     | None -> CoFixpoint, true, []
@@ -269,13 +269,13 @@ let declare_fixpoint_interactive_generic ?indexes local poly ((fixnames,_fixrs,f
     Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC) fixdefs) in
   let evd = Evd.from_ctx ctx in
   let lemma =
-    Lemmas.start_lemma_with_initialization ~poly ~kind:(local,DefinitionBody fix_kind) ~udecl
+    Lemmas.start_lemma_with_initialization ~poly ~scope ~kind:(DefinitionBody fix_kind) ~udecl
       evd (Some(cofix,indexes,init_tac)) thms None in
   (* Declare notations *)
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
   lemma
 
-let declare_fixpoint_generic ?indexes local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
+let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
   let indexes, cofix, fix_kind =
     match indexes with
     | Some indexes -> indexes, false, Fixpoint
@@ -303,7 +303,7 @@ let declare_fixpoint_generic ?indexes local poly ((fixnames,fixrs,fixdefs,fixtyp
   let pl = Evd.universe_binders evd in
   let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in
   let fixdecls = List.map mk_pure fixdecls in
-  ignore (List.map4 (DeclareDef.declare_fix (local, poly, fix_kind) pl ctx)
+  ignore (List.map4 (fun name -> DeclareDef.declare_fix ~name ~scope ~kind:fix_kind pl ctx)
             fixnames fixdecls fixtypes fiximps);
   recursive_message (not cofix) gidx fixnames;
   List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
@@ -351,28 +351,28 @@ let do_fixpoint_common l =
   let (_, _, _, info as fix) = interp_fixpoint ~cofix:false fixl ntns in
   fixl, ntns, fix, List.map compute_possible_guardness_evidences info
 
-let do_fixpoint_interactive local poly l : Lemmas.t =
+let do_fixpoint_interactive ~scope ~poly l : Lemmas.t =
   let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
-  let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes local poly fix ntns in
+  let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ~poly fix ntns in
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
   lemma
 
-let do_fixpoint local poly l =
+let do_fixpoint ~scope ~poly l =
   let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
-  declare_fixpoint_generic ~indexes:possible_indexes local poly fix ntns;
+  declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns;
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
 
 let do_cofixpoint_common l =
   let fixl,ntns = extract_cofixpoint_components l in
   ntns, interp_fixpoint ~cofix:true fixl ntns
 
-let do_cofixpoint_interactive local poly l =
+let do_cofixpoint_interactive ~scope ~poly l =
   let ntns, cofix = do_cofixpoint_common l in
-  let lemma = declare_fixpoint_interactive_generic local poly cofix ntns in
+  let lemma = declare_fixpoint_interactive_generic ~scope ~poly cofix ntns in
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ();
   lemma
 
-let do_cofixpoint local poly l =
+let do_cofixpoint ~scope ~poly l =
   let ntns, cofix = do_cofixpoint_common l in
-  declare_fixpoint_generic local poly cofix ntns;
+  declare_fixpoint_generic ~scope ~poly cofix ntns;
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 8d76a30cee..c04cc95837 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -19,16 +19,16 @@ open Vernacexpr
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint_interactive :
-  locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> Lemmas.t
+  scope:locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> Lemmas.t
 
 val do_fixpoint :
-  locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
+  scope:locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit
 
 val do_cofixpoint_interactive :
-  locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> Lemmas.t
+  scope:locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> Lemmas.t
 
 val do_cofixpoint :
-  locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
+  scope:locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit
 
 (************************************************************************)
 (** Internal API  *)
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 6c1c23eacb..d804957917 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -234,8 +234,8 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
     Obligations.eterm_obligations env recname sigma 0 def typ
   in
   let ctx = Evd.evar_universe_context sigma in
-    ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl
-             evars_typ ctx evars ~hook)
+    ignore(Obligations.add_definition ~name:recname ~term:evars_def ~univdecl:decl
+             ~poly evars_typ ctx evars ~hook)
 
 let out_def = function
   | Some def -> def
@@ -246,7 +246,7 @@ let collect_evars_of_term evd c ty =
   Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
   evars (Evd.from_ctx (Evd.evar_universe_context evd))
 
-let do_program_recursive local poly fixkind fixl ntns =
+let do_program_recursive ~scope ~poly fixkind fixl ntns =
   let cofix = fixkind = DeclareObl.IsCoFixpoint in
   let (env, rec_sign, pl, evd), fix, info =
     interp_recursive ~cofix ~program_mode:true fixl ntns
@@ -288,12 +288,12 @@ let do_program_recursive local poly fixkind fixl ntns =
   end in
   let ctx = Evd.evar_universe_context evd in
   let kind = match fixkind with
-  | DeclareObl.IsFixpoint _ -> (local, poly, Fixpoint)
-  | DeclareObl.IsCoFixpoint -> (local, poly, CoFixpoint)
+  | DeclareObl.IsFixpoint _ -> Fixpoint
+  | DeclareObl.IsCoFixpoint -> CoFixpoint
   in
-  Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind
+  Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~univdecl:pl ctx ntns fixkind
 
-let do_program_fixpoint local poly l =
+let do_program_fixpoint ~scope ~poly l =
   let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
     match g, l with
     | [Some { CAst.v = CWfRec (n,r) }], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
@@ -316,7 +316,7 @@ let do_program_fixpoint local poly l =
     | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g ->
         let fixl,ntns = extract_fixpoint_components ~structonly:true l in
         let fixkind = DeclareObl.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in
-          do_program_recursive local poly fixkind fixl ntns
+          do_program_recursive ~scope ~poly fixkind fixl ntns
 
     | _, _ ->
         user_err ~hdr:"do_program_fixpoint"
@@ -334,11 +334,11 @@ let check_safe () =
   let flags = Environ.typing_flags (Global.env ()) in
   flags.check_universes && flags.check_guarded
 
-let do_fixpoint local poly l =
-  do_program_fixpoint local poly l;
+let do_fixpoint ~scope ~poly l =
+  do_program_fixpoint ~scope ~poly l;
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
 
-let do_cofixpoint local poly l =
+let do_cofixpoint ~scope ~poly l =
   let fixl,ntns = extract_cofixpoint_components l in
-  do_program_recursive local poly DeclareObl.IsCoFixpoint fixl ntns;
+  do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl ntns;
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli
index 943cb8efe6..ba735f9c10 100644
--- a/vernac/comProgramFixpoint.mli
+++ b/vernac/comProgramFixpoint.mli
@@ -5,8 +5,8 @@ open Vernacexpr
 
 val do_fixpoint :
   (* When [false], assume guarded. *)
-  locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
+  scope:locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> unit
 
 val do_cofixpoint :
   (* When [false], assume guarded. *)
-  locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
+  scope:locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index a467c22ede..e82fb3e3b1 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -36,31 +36,31 @@ module Hook = struct
 end
 
 (* Locality stuff *)
-let declare_definition ident (local, p, k) ?hook_data ce pl imps =
+let declare_definition ~name ~scope ~kind ?hook_data udecl ce imps =
   let fix_exn = Future.fix_exn_of ce.Proof_global.proof_entry_body in
-  let gr = match local with
+  let gr = match scope with
   | Discharge ->
-      let _ = declare_variable ident (Lib.cwd(), SectionLocalDef ce, IsDefinition k) in
-      VarRef ident
+      let _ = declare_variable name (Lib.cwd(), SectionLocalDef ce, IsDefinition kind) in
+      VarRef name
   | Global local ->
-      let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in
+      let kn = declare_constant name ~local (DefinitionEntry ce, IsDefinition kind) in
       let gr = ConstRef kn in
-      let () = Declare.declare_univ_binders gr pl in
+      let () = Declare.declare_univ_binders gr udecl in
       gr
   in
   let () = maybe_declare_manual_implicits false gr imps in
-  let () = definition_message ident in
+  let () = definition_message name in
   begin
     match hook_data with
     | None -> ()
     | Some (hook, uctx, extra_defs) ->
-      Hook.call ~fix_exn ~hook uctx extra_defs local gr
+      Hook.call ~fix_exn ~hook uctx extra_defs scope gr
   end;
   gr
 
-let declare_fix ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps =
+let declare_fix ?(opaque = false) ?hook_data ~name ~scope ~kind udecl univs ((def,_),eff) t imps =
   let ce = definition_entry ~opaque ~types:t ~univs ~eff def in
-  declare_definition f kind ?hook_data ce pl imps
+  declare_definition ~name ~scope ~kind ?hook_data udecl ce imps
 
 let check_definition_evars ~allow_evars sigma =
   let env = Global.env () in
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index ac4f44608b..708158814e 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -40,21 +40,23 @@ module Hook : sig
 end
 
 val declare_definition
-  : Id.t
-  -> definition_kind
+  :  name:Id.t
+  -> scope:locality
+  -> kind:definition_object_kind
   -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
-  -> Evd.side_effects Proof_global.proof_entry
   -> UnivNames.universe_binders
+  -> Evd.side_effects Proof_global.proof_entry
   -> Impargs.manual_implicits
   -> GlobRef.t
 
 val declare_fix
-  : ?opaque:bool
+  :  ?opaque:bool
   -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
-  -> definition_kind
+  -> name:Id.t
+  -> scope:locality
+  -> kind:definition_object_kind
   -> UnivNames.universe_binders
   -> Entries.universes_entry
-  -> Id.t
   -> Evd.side_effects Entries.proof_output
   -> Constr.types
   -> Impargs.manual_implicits
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 4936c9838d..1790932c23 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -48,7 +48,9 @@ type program_info =
   ; prg_fixkind : fixpoint_kind option
   ; prg_implicits : Impargs.manual_implicits
   ; prg_notations : notations
-  ; prg_kind : definition_kind
+  ; prg_poly : bool
+  ; prg_scope : locality
+  ; prg_kind : definition_object_kind
   ; prg_reduce : constr -> constr
   ; prg_hook : DeclareDef.Hook.t option
   ; prg_opaque : bool
@@ -146,7 +148,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_poly in
     let ctx, body, ty, args =
       if get_shrink_obligations () && not poly then shrink_body body ty
       else ([], body, ty, [||])
@@ -355,13 +357,14 @@ let declare_definition prg =
   in
   let uctx = UState.restrict prg.prg_ctx uvars in
   let univs =
-    UState.check_univ_decl ~poly:(pi2 prg.prg_kind) uctx prg.prg_univdecl
+    UState.check_univ_decl ~poly:prg.prg_poly uctx prg.prg_univdecl
   in
   let ce = Declare.definition_entry ~fix_exn ~opaque ~types:typ ~univs body in
   let () = progmap_remove prg in
   let ubinders = UState.universe_binders uctx in
   let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in
-  DeclareDef.declare_definition prg.prg_name prg.prg_kind ce ubinders
+  DeclareDef.declare_definition
+    ~name:prg.prg_name ~scope:prg.prg_scope ubinders ~kind:prg.prg_kind ce
     prg.prg_implicits ?hook_data
 
 let rec lam_index n t acc =
@@ -418,7 +421,6 @@ let declare_mutual_definition l =
   let rvec = Array.of_list fixrs in
   let namevec = Array.of_list (List.map (fun x -> Name x.prg_name) l) in
   let fixdecls = (Array.map2 make_annot namevec rvec, 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
@@ -438,12 +440,14 @@ let declare_mutual_definition l =
       (None, List.map_i (fun i _ -> mk_proof (mkCoFix (i, fixdecls))) 0 l)
   in
   (* Declare the recursive definitions *)
+  let poly = first.prg_poly in
+  let scope = first.prg_scope in
   let univs = UState.univ_entry ~poly first.prg_ctx in
   let fix_exn = Hook.get get_fix_exn () in
   let kns =
     List.map4
-      (DeclareDef.declare_fix ~opaque (local, poly, kind)
-         UnivNames.empty_binders univs)
+      (fun name -> DeclareDef.declare_fix ~name ~opaque ~scope ~kind
+          UnivNames.empty_binders univs)
       fixnames fixdecls fixtypes fiximps
   in
   (* Declare notations *)
@@ -452,7 +456,7 @@ let declare_mutual_definition l =
     first.prg_notations;
   Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
   let gr = List.hd kns in
-  DeclareDef.Hook.call ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr;
+  DeclareDef.Hook.call ?hook:first.prg_hook ~fix_exn first.prg_ctx obls scope gr;
   List.iter progmap_remove l;
   gr
 
@@ -523,15 +527,15 @@ let obligation_terminator opq entries uctx { name; num; auto } =
     in
     let obl = { obl with obl_status = false, status } in
     let ctx =
-      if pi2 prg.prg_kind then ctx
+      if prg.prg_poly then ctx
       else UState.union prg.prg_ctx ctx
     in
-    let uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) ctx in
+    let uctx = UState.univ_entry ~poly:prg.prg_poly ctx in
     let (defined, obl) = declare_obligation prg obl body ty uctx in
     let obls = Array.copy obls in
     let () = obls.(num) <- obl in
     let prg_ctx =
-      if pi2 (prg.prg_kind) then (* Polymorphic *)
+      if prg.prg_poly then (* Polymorphic *)
         (* We merge the new universes and constraints of the
            polymorphic obligation with the existing ones *)
         UState.union prg.prg_ctx ctx
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
index f4495181b3..4774d73aa7 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -42,7 +42,9 @@ type program_info =
   ; prg_fixkind : fixpoint_kind option
   ; prg_implicits : Impargs.manual_implicits
   ; prg_notations : notations
-  ; prg_kind : Decl_kinds.definition_kind
+  ; prg_poly : bool
+  ; prg_scope : Decl_kinds.locality
+  ; prg_kind : Decl_kinds.definition_object_kind
   ; prg_reduce : constr -> constr
   ; prg_hook : DeclareDef.Hook.t option
   ; prg_opaque : bool
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 744cdbfb5f..aa3145bc5a 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -74,14 +74,18 @@ module Info = struct
     ; proof_ending : Proof_ending.t CEphemeron.key
     (* This could be improved and the CEphemeron removed *)
     ; other_thms : Recthm.t list
+    ; scope : Decl_kinds.locality
+    ; kind : Decl_kinds.goal_object_kind
     }
 
-  let make ?hook ?(proof_ending=Proof_ending.Regular) () =
+  let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=Global ImportDefaultBehavior) ?(kind=Proof Lemma) () =
     { hook
     ; compute_guard = []
     ; impargs = []
     ; proof_ending = CEphemeron.create proof_ending
     ; other_thms = []
+    ; scope
+    ; kind
     }
 end
 
@@ -246,13 +250,13 @@ let check_name_freshness locality {CAst.loc;v=id} : unit =
   then
     user_err ?loc  (Id.print id ++ str " already exists.")
 
-let save_remaining_recthms env sigma ~poly (locality,kind) norm univs body opaq i
+let save_remaining_recthms env sigma ~poly ~scope norm univs body opaq i
     { Recthm.name; typ; impargs } =
   let t_i = norm typ in
   let k = IsAssumption Conjectural in
   match body with
   | None ->
-      (match locality with
+      (match scope with
       | Discharge ->
           let impl = false in (* copy values from Vernacentries *)
           let univs = match univs with
@@ -271,7 +275,6 @@ let save_remaining_recthms env sigma ~poly (locality,kind) norm univs body opaq
           (ConstRef kn,impargs))
   | Some body ->
       let body = norm body in
-      let k = Kindops.logical_kind_of_goal_kind kind in
       let rec body_i t = match Constr.kind t with
         | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
         | CoFix (0,decls) -> mkCoFix (i,decls)
@@ -281,7 +284,7 @@ let save_remaining_recthms env sigma ~poly (locality,kind) norm univs body opaq
         | _ ->
           anomaly Pp.(str "Not a proof by induction: " ++ Printer.pr_constr_env env sigma body ++ str ".") in
       let body_i = body_i body in
-      match locality with
+      match scope with
       | Discharge ->
           let const = definition_entry ~types:t_i ~opaque:opaq ~univs body_i in
           let c = SectionLocalDef const in
@@ -338,19 +341,19 @@ module Stack = struct
 end
 
 (* Starting a goal *)
-let start_lemma ~name ~poly ~kind
+let start_lemma ~name ~poly
     ?(udecl=UState.default_univ_decl)
     ?(sign=initialize_named_context_for_proof())
     ?(info=Info.make ())
     sigma c =
   let goals = [ Global.env_of_context sign , c ] in
-  let proof = Proof_global.start_proof sigma ~name ~udecl ~poly ~kind goals in
+  let proof = Proof_global.start_proof sigma ~name ~udecl ~poly goals in
   { proof ; info }
 
-let start_dependent_lemma ~name ~poly ~kind
+let start_dependent_lemma ~name ~poly
     ?(udecl=UState.default_univ_decl)
     ?(info=Info.make ()) telescope =
-  let proof = Proof_global.start_dependent_proof ~name ~udecl ~poly ~kind telescope in
+  let proof = Proof_global.start_dependent_proof ~name ~udecl ~poly telescope in
   { proof; info }
 
 let rec_tac_initializer finite guard thms snl =
@@ -367,7 +370,7 @@ let rec_tac_initializer finite guard thms snl =
        | (id,n,_)::l -> Tactics.mutual_fix id n l 0
        | _ -> assert false
 
-let start_lemma_with_initialization ?hook ~poly ~kind ~udecl sigma recguard thms snl =
+let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recguard thms snl =
   let intro_tac { Recthm.args; _ } = Tactics.auto_intros_tac args in
   let init_tac, compute_guard = match recguard with
   | Some (finite,guard,init_tac) ->
@@ -391,14 +394,16 @@ let start_lemma_with_initialization ?hook ~poly ~kind ~udecl sigma recguard thms
            ; compute_guard
            ; other_thms
            ; proof_ending = CEphemeron.create Proof_ending.Regular
+           ; scope
+           ; kind
            } in
-    let lemma = start_lemma ~name ~poly ~kind ~udecl ~info sigma typ in
+    let lemma = start_lemma ~name ~poly ~udecl ~info sigma typ in
     pf_map (Proof_global.map_proof (fun p ->
         match init_tac with
         | None -> p
         | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p)) lemma
 
-let start_lemma_com ~program_mode ~poly ~kind ?inference_hook ?hook thms =
+let start_lemma_com ~program_mode ~poly ~scope ~kind ?inference_hook ?hook thms =
   let env0 = Global.env () in
   let decl = fst (List.hd thms) in
   let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
@@ -409,7 +414,7 @@ let start_lemma_com ~program_mode ~poly ~kind ?inference_hook ?hook thms =
     let hook = inference_hook in
     let evd = solve_remaining_evars ?hook flags env evd in
     let ids = List.map RelDecl.get_name ctx in
-    check_name_freshness (fst kind) id;
+    check_name_freshness scope id;
     (* XXX: The nf_evar is critical !! *)
     evd, (id.CAst.v,
           (Evarutil.nf_evar evd (EConstr.it_mkProd_or_LetIn t' ctx),
@@ -431,7 +436,7 @@ let start_lemma_com ~program_mode ~poly ~kind ?inference_hook ?hook thms =
     else (* We fix the variables to ensure they won't be lowered to Set *)
       Evd.fix_undefined_variables evd
   in
-  start_lemma_with_initialization ?hook ~poly ~kind evd ~udecl recguard thms snl
+  start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl
 
 (************************************************************************)
 (* Admitting a lemma-like constant                                      *)
@@ -449,19 +454,19 @@ let warn_let_as_axiom =
 
 (* This declares implicits and calls the hooks for all the theorems,
    including the main one *)
-let process_recthms ?fix_exn ?hook env sigma ctx decl ~poly strength ref imps other_thms =
+let process_recthms ?fix_exn ?hook env sigma ctx ~udecl ~poly ~scope ref imps other_thms =
   let other_thms_data =
     if List.is_empty other_thms then [] else
       (* there are several theorems defined mutually *)
       let body,opaq = retrieve_first_recthm ctx ref in
       let norm c = EConstr.to_constr (Evd.from_ctx ctx) c in
       let body = Option.map EConstr.of_constr body in
-      let uctx = UState.check_univ_decl ~poly ctx decl in
-      List.map_i (save_remaining_recthms env sigma ~poly strength norm uctx body opaq) 1 other_thms in
+      let uctx = UState.check_univ_decl ~poly ctx udecl in
+      List.map_i (save_remaining_recthms env sigma ~poly ~scope norm uctx body opaq) 1 other_thms in
   let thms_data = (ref,imps)::other_thms_data in
   List.iter (fun (ref,imps) ->
       maybe_declare_manual_implicits false ref imps;
-      DeclareDef.Hook.call ?fix_exn ?hook ctx [] (fst strength) ref) thms_data
+      DeclareDef.Hook.call ?fix_exn ?hook ctx [] scope ref) thms_data
 
 let get_keep_admitted_vars =
   Goptions.declare_bool_option_and_ref
@@ -470,7 +475,7 @@ let get_keep_admitted_vars =
     ~key:["Keep"; "Admitted"; "Variables"]
     ~value:true
 
-let finish_admitted env sigma id ~poly (scope,kind) pe ctx hook udecl impargs other_thms =
+let finish_admitted env sigma id ~poly ~scope pe ctx hook ~udecl impargs other_thms =
   let local = match scope with
   | Global local -> local
   | Discharge -> warn_let_as_axiom id; ImportNeedQualified
@@ -479,14 +484,14 @@ let finish_admitted env sigma id ~poly (scope,kind) pe ctx hook udecl impargs ot
   let () = assumption_message id in
   Declare.declare_univ_binders (ConstRef kn) (UState.universe_binders ctx);
   (* This takes care of the implicits and hook for the current constant*)
-  process_recthms ?fix_exn:None ?hook env sigma ctx udecl ~poly (Global local,kind) (ConstRef kn) impargs other_thms;
+  process_recthms ?fix_exn:None ?hook env sigma ctx ~udecl ~poly ~scope:(Global local) (ConstRef kn) impargs other_thms;
   Feedback.feedback Feedback.AddedAxiom
 
 let save_lemma_admitted ?proof ~(lemma : t) =
     let open Proof_global in
     let env = Global.env () in
     match proof with
-    | Some ({ id; entries; persistence = k; universes; udecl }, { Info.hook; impargs; other_thms; _} ) ->
+    | Some ({ id; entries; universes; udecl }, { Info.hook; scope; impargs; other_thms; _} ) ->
       if List.length entries <> 1 then
         user_err Pp.(str "Admitted does not support multiple statements");
       let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
@@ -499,10 +504,10 @@ let save_lemma_admitted ?proof ~(lemma : t) =
       let ctx = UState.univ_entry ~poly universes in
       let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
       let sigma = Evd.from_env env in
-      finish_admitted env sigma id k (sec_vars, (typ, ctx), None) universes hook ~poly udecl impargs other_thms
+      finish_admitted env sigma id ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms
     | None ->
       let pftree = Proof_global.get_proof lemma.proof in
-      let gk = Proof_global.get_persistence lemma.proof in
+      let scope = lemma.info.Info.scope in
       let Proof.{ name; poly; entry } = Proof.data pftree in
       let typ = match Proofview.initial_goals entry with
         | [typ] -> snd typ
@@ -529,7 +534,7 @@ let save_lemma_admitted ?proof ~(lemma : t) =
       let { Info.hook; impargs; other_thms } = lemma.info in
       let { Proof.sigma } = Proof.data (Proof_global.get_proof lemma.proof) in
       let ctx = UState.check_univ_decl ~poly universes udecl in
-      finish_admitted env sigma name gk (sec_vars, (typ, ctx), None) universes hook ~poly udecl impargs other_thms
+      finish_admitted env sigma name ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms
 
 (************************************************************************)
 (* Saving a lemma-like constant                                         *)
@@ -537,9 +542,9 @@ let save_lemma_admitted ?proof ~(lemma : t) =
 
 let finish_proved env sigma opaque idopt po info =
   let open Proof_global in
-  let { Info.hook; compute_guard; impargs; other_thms } = info in
+  let { Info.hook; compute_guard; impargs; other_thms; scope; kind } = info in
   match po with
-  | { id; entries=[const]; persistence=locality,kind; universes; udecl; poly } ->
+  | { id; entries=[const]; universes; udecl; poly } ->
     let is_opaque = match opaque with
       | Transparent -> false
       | Opaque      -> true
@@ -553,7 +558,7 @@ let finish_proved env sigma opaque idopt po info =
       let const = adjust_guardness_conditions const compute_guard in
       let k = Kindops.logical_kind_of_goal_kind kind in
       let should_suggest = const.proof_entry_opaque && Option.is_empty const.proof_entry_secctx in
-      let r = match locality with
+      let r = match scope with
         | Discharge ->
           let c = SectionLocalDef const in
           let _ = declare_variable id (Lib.cwd(), c, k) in
@@ -573,7 +578,7 @@ let finish_proved env sigma opaque idopt po info =
       in
       definition_message id;
       (* This takes care of the implicits and hook for the current constant*)
-      process_recthms ~fix_exn ?hook env sigma universes udecl ~poly (locality,kind) r impargs other_thms
+      process_recthms ~fix_exn ?hook env sigma universes ~udecl ~poly ~scope r impargs other_thms
     with e when CErrors.noncritical e ->
       let e = CErrors.push e in
       iraise (fix_exn e)
@@ -626,11 +631,11 @@ let finish_derived ~f ~name ~idopt ~opaque ~entries =
   in
   ignore (Declare.declare_constant name lemma_def)
 
-let finish_proved_equations opaque lid proof_obj hook i types wits sigma0 =
+let finish_proved_equations opaque lid kind proof_obj hook i types wits sigma0 =
 
   let open Decl_kinds in
   let obls = ref 1 in
-  let kind = match snd proof_obj.Proof_global.persistence with
+  let kind = match kind with
     | DefinitionBody d -> IsDefinition d
     | Proof p -> IsProof p
   in
@@ -678,4 +683,4 @@ let save_lemma_proved ?proof ?lemma ~opaque ~idopt =
   | End_derive { f ; name } ->
     finish_derived ~f ~name ~idopt ~opaque ~entries:proof_obj.entries
   | End_equations { hook; i; types; wits; sigma } ->
-    finish_proved_equations opaque idopt proof_obj hook i types wits sigma
+    finish_proved_equations opaque idopt proof_info.Info.kind proof_obj hook i types wits sigma
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 1a8b1f2f30..a3df43f80e 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -85,6 +85,10 @@ module Info : sig
     (** Callback to be executed at the end of the proof *)
     -> ?proof_ending : Proof_ending.t
     (** Info for special constants *)
+    -> ?scope : Decl_kinds.locality
+    (** locality  *)
+    -> ?kind:goal_object_kind
+    (** Theorem, etc... *)
     -> unit
     -> t
 
@@ -94,7 +98,6 @@ end
 val start_lemma
   :  name:Id.t
   -> poly:bool
-  -> kind:goal_kind
   -> ?udecl:UState.universe_decl
   -> ?sign:Environ.named_context_val
   -> ?info:Info.t
@@ -105,7 +108,6 @@ val start_lemma
 val start_dependent_lemma
   :  name:Id.t
   -> poly:bool
-  -> kind:goal_kind
   -> ?udecl:UState.universe_decl
   -> ?info:Info.t
   -> Proofview.telescope
@@ -117,7 +119,8 @@ type lemma_possible_guards = int list list
 val start_lemma_with_initialization
   :  ?hook:DeclareDef.Hook.t
   -> poly:bool
-  -> kind:goal_kind
+  -> scope:locality
+  -> kind:goal_object_kind
   -> udecl:UState.universe_decl
   -> Evd.evar_map
   -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option
@@ -131,7 +134,8 @@ val default_thm_id : Names.Id.t
 val start_lemma_com
   :  program_mode:bool
   -> poly:bool
-  -> kind:goal_kind
+  -> scope:locality
+  -> kind:goal_object_kind
   -> ?inference_hook:Pretyping.inference_hook
   -> ?hook:DeclareDef.Hook.t
   -> Vernacexpr.proof_expr list
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index b2c5520c0b..ba514f9ab3 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -300,7 +300,7 @@ let add_hint local prg cst =
   Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst)
 
 let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind
-                   notations obls impls kind reduce =
+                   notations obls impls ~scope ~poly ~kind reduce =
   let obls', b =
     match b with
     | None ->
@@ -320,13 +320,23 @@ let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind
 	  obls, b
   in
   let ctx = UState.make_flexible_nonalgebraic ctx in
-    { prg_name = n ; prg_body = b; prg_type = reduce t;
-      prg_ctx = ctx; prg_univdecl = udecl;
-      prg_obligations = (obls', Array.length obls');
-      prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
-      prg_implicits = impls; prg_kind = kind; prg_reduce = reduce;
-      prg_hook = hook; prg_opaque = opaque;
-      prg_sign = sign }
+    { prg_name = n
+    ; prg_body = b
+    ; prg_type = reduce t
+    ; prg_ctx = ctx
+    ; prg_univdecl = udecl
+    ; prg_obligations = (obls', Array.length obls')
+    ; prg_deps = deps
+    ; prg_fixkind = fixkind
+    ; prg_notations = notations
+    ; prg_implicits = impls
+    ; prg_poly = poly
+    ; prg_scope = scope
+    ; prg_kind = kind
+    ; prg_reduce = reduce
+    ; prg_hook = hook
+    ; prg_opaque = opaque
+    ; prg_sign = sign }
 
 let map_cardinal m =
   let i = ref 0 in
@@ -408,12 +418,11 @@ let warn_solve_errored = CWarnings.create ~name:"solve_obligation_error" ~catego
             str "This will become an error in the future"])
 
 let solve_by_tac ?loc name evi t poly ctx =
-  let id = name in
   (* spiwack: the status is dropped. *)
   try
     let (entry,_,ctx') =
       Pfedit.build_constant_by_tactic
-        id ~poly ~goal_kind ctx evi.evar_hyps evi.evar_concl t in
+        ~name ~poly ctx evi.evar_hyps evi.evar_concl t in
     let env = Global.env () in
     let (body, eff) = Future.force entry.Proof_global.proof_entry_body in
     let body = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
@@ -443,7 +452,7 @@ let obligation_hook prg obl num auto ctx' _ _ gr =
     | _ -> ()
   in
   let inst, ctx' =
-    if not (pi2 prg.prg_kind) (* Not polymorphic *) then
+    if not prg.prg_poly (* Not polymorphic *) then
       (* The universe context was declared globally, we continue
          from the new global environment. *)
       let ctx = UState.make (Global.universes ()) in
@@ -484,15 +493,15 @@ 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 (snd obl.obl_status) in
+  let scope, kind = kind_of_obligation (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 oblset tac = auto_solve_obligations n ~oblset tac in
   let proof_ending = Lemmas.Proof_ending.End_obligation (DeclareObl.{name = prg.prg_name; num; auto}) in
   let hook = DeclareDef.Hook.make (obligation_hook prg obl num auto) in
-  let info = Lemmas.Info.make ~hook ~proof_ending () in
-  let poly = pi2 prg.prg_kind in
-  let lemma = Lemmas.start_lemma ~sign:prg.prg_sign ~name:obl.obl_name ~poly ~kind ~info evd (EConstr.of_constr obl.obl_type) in
+  let info = Lemmas.Info.make ~hook ~proof_ending ~scope ~kind () in
+  let poly = prg.prg_poly in
+  let lemma = Lemmas.start_lemma ~sign:prg.prg_sign ~name:obl.obl_name ~poly ~info evd (EConstr.of_constr obl.obl_type) in
   let lemma = fst @@ Lemmas.by !default_tactic lemma in
   let lemma = Option.cata (fun tac -> Lemmas.set_endline_tactic tac lemma) lemma tac in
   lemma
@@ -527,14 +536,14 @@ and solve_obligation_by_tac prg obls i tac =
         let evd = Evd.from_ctx prg.prg_ctx in
         let evd = Evd.update_sigma_env evd (Global.env ()) in
         match solve_by_tac ?loc:(fst obl.obl_location) obl.obl_name (evar_of_obligation obl) tac
-                (pi2 prg.prg_kind) (Evd.evar_universe_context evd) with
+                prg.prg_poly (Evd.evar_universe_context evd) with
         | None -> None
         | Some (t, ty, ctx) ->
-          let uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) ctx in
+          let uctx = UState.univ_entry ~poly:prg.prg_poly 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_poly 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
@@ -628,12 +637,12 @@ let show_term n =
              Printer.pr_constr_env env sigma prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
             ++ Printer.pr_constr_env env sigma prg.prg_body)
 
-let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
-                   ?(implicits=[]) ?(kind=Global ImportDefaultBehavior,false,Definition) ?tactic
+let add_definition ~name ?term t ctx ?(univdecl=UState.default_univ_decl)
+                   ?(implicits=[]) ~poly ?(scope=Global ImportDefaultBehavior) ?(kind=Definition) ?tactic
     ?(reduce=reduce) ?hook ?(opaque = false) obls =
   let sign = Lemmas.initialize_named_context_for_proof () in
-  let info = Id.print n ++ str " has type-checked" in
-  let prg = init_prog_info sign ~opaque n univdecl term t ctx [] None [] obls implicits kind reduce ?hook in
+  let info = Id.print name ++ str " has type-checked" in
+  let prg = init_prog_info sign ~opaque name univdecl term t ctx [] None [] obls implicits ~poly ~scope ~kind reduce ?hook in
   let obls,_ = prg.prg_obligations in
   if Int.equal (Array.length obls) 0 then (
     Flags.if_verbose Feedback.msg_info (info ++ str ".");
@@ -642,21 +651,21 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
   else (
     let len = Array.length obls in
     let () = Flags.if_verbose Feedback.msg_info (info ++ str ", generating " ++ int len ++ str (String.plural len " obligation")) in
-      progmap_add n (CEphemeron.create prg);
-      let res = auto_solve_obligations (Some n) tactic in
+      progmap_add name (CEphemeron.create prg);
+      let res = auto_solve_obligations (Some name) tactic in
 	match res with
-	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
+        | Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some name)) (); res
 	| _ -> res)
 
 let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
-                           ?(kind=Global ImportDefaultBehavior,false,Definition) ?(reduce=reduce)
+                           ~poly ?(scope=Global ImportDefaultBehavior) ?(kind=Definition) ?(reduce=reduce)
     ?hook ?(opaque = false) notations fixkind =
   let sign = Lemmas.initialize_named_context_for_proof () in
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
     List.iter
     (fun  (n, b, t, imps, obls) ->
      let prg = init_prog_info sign ~opaque n univdecl (Some b) t ctx deps (Some fixkind)
-       notations obls imps kind reduce ?hook
+       notations obls imps ~poly ~scope ~kind reduce ?hook
      in progmap_add n (CEphemeron.create prg)) l;
     let _defined =
       List.fold_left (fun finished x ->
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index a0010a5026..787ab53e66 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -43,12 +43,14 @@ type obligation_info =
 val default_tactic : unit Proofview.tactic ref
 
 val add_definition
-  :  Names.Id.t
+  :  name:Names.Id.t
   -> ?term:constr -> types
   -> UState.t
   -> ?univdecl:UState.universe_decl (* Universe binders and constraints *)
   -> ?implicits:Impargs.manual_implicits
-  -> ?kind:Decl_kinds.definition_kind
+  -> poly:bool
+  -> ?scope:Decl_kinds.locality
+  -> ?kind:Decl_kinds.definition_object_kind
   -> ?tactic:unit Proofview.tactic
   -> ?reduce:(constr -> constr)
   -> ?hook:DeclareDef.Hook.t
@@ -56,16 +58,19 @@ val add_definition
   -> obligation_info
   -> DeclareObl.progress
 
-val add_mutual_definitions :
-  (Names.Id.t * constr * types * Impargs.manual_implicits * obligation_info) list ->
-  UState.t ->
-  ?univdecl:UState.universe_decl -> (* Universe binders and constraints *)
-  ?tactic:unit Proofview.tactic ->
-  ?kind:Decl_kinds.definition_kind ->
-  ?reduce:(constr -> constr) ->
-  ?hook:DeclareDef.Hook.t -> ?opaque:bool ->
-  DeclareObl.notations ->
-  DeclareObl.fixpoint_kind -> unit
+val add_mutual_definitions
+  : (Names.Id.t * constr * types * Impargs.manual_implicits * obligation_info) list
+  -> UState.t
+  -> ?univdecl:UState.universe_decl
+  (** Universe binders and constraints *)
+  -> ?tactic:unit Proofview.tactic
+  -> poly:bool
+  -> ?scope:Decl_kinds.locality
+  -> ?kind:Decl_kinds.definition_object_kind
+  -> ?reduce:(constr -> constr)
+  -> ?hook:DeclareDef.Hook.t -> ?opaque:bool
+  -> DeclareObl.notations
+  -> DeclareObl.fixpoint_kind -> unit
 
 val obligation
   :  int * Names.Id.t option * Constrexpr.constr_expr option
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index d1377fecc5..ee00bc0e2a 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -560,7 +560,7 @@ let () =
 (***********)
 (* Gallina *)
 
-let start_proof_and_print ~program_mode ~poly ?hook k l =
+let start_proof_and_print ~program_mode ~poly ?hook ~scope ~kind l =
   let inference_hook =
     if program_mode then
       let hook env sigma ev =
@@ -582,7 +582,7 @@ let start_proof_and_print ~program_mode ~poly ?hook k l =
       in Some hook
     else None
   in
-  start_lemma_com ~program_mode ?inference_hook ?hook ~poly ~kind:k l
+  start_lemma_com ~program_mode ?inference_hook ?hook ~poly ~scope ~kind l
 
 let vernac_definition_hook p = function
 | Coercion ->
@@ -616,30 +616,30 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
   let program_mode = atts.program in
   let poly = atts.polymorphic in
   let name = vernac_definition_name lid local in
-  start_proof_and_print ~program_mode ~poly (local, DefinitionBody kind) ?hook [(name, pl), (bl, t)]
+  start_proof_and_print ~program_mode ~poly ~scope:local ~kind:(DefinitionBody kind) ?hook [(name, pl), (bl, t)]
 
 let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt =
   let open DefAttributes in
-  let local = enforce_locality_exp atts.locality discharge in
+  let scope = enforce_locality_exp atts.locality discharge in
   let hook = vernac_definition_hook atts.polymorphic kind in
   let program_mode = atts.program in
-  let name = vernac_definition_name lid local in
+  let name = vernac_definition_name lid scope in
   let red_option = match red_option with
     | None -> None
     | Some r ->
       let env = Global.env () in
       let sigma = Evd.from_env env in
       Some (snd (Hook.get f_interp_redexp env sigma r)) in
-  ComDefinition.do_definition ~program_mode name.v
-    (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook
+  ComDefinition.do_definition ~program_mode ~name:name.v
+    ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook
 
 (* NB: pstate argument to use combinators easily *)
 let vernac_start_proof ~atts kind l =
   let open DefAttributes in
-  let local = enforce_locality_exp atts.locality NoDischarge in
+  let scope = enforce_locality_exp atts.locality NoDischarge in
   if Dumpglob.dump () then
     List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l;
-  start_proof_and_print ~program_mode:atts.program ~poly:atts.polymorphic (local, Proof kind) l
+  start_proof_and_print ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Proof kind) l
 
 let vernac_end_proof ?stack ?proof = let open Vernacexpr in function
   | Admitted ->
@@ -666,15 +666,14 @@ let vernac_exact_proof ~lemma c =
 
 let vernac_assumption ~atts discharge kind l nl =
   let open DefAttributes in
-  let local = enforce_locality_exp atts.locality discharge in
-  let kind = local, atts.polymorphic, kind in
+  let scope = enforce_locality_exp atts.locality discharge in
   List.iter (fun (is_coe,(idl,c)) ->
     if Dumpglob.dump () then
       List.iter (fun (lid, _) ->
-          match local with
+          match scope with
             | Global _ -> Dumpglob.dump_definition lid false "ax"
             | Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
-  let status = ComAssumption.do_assumptions ~program_mode:atts.program kind nl l in
+  let status = ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l in
   if not status then Feedback.feedback Feedback.AddedAxiom
 
 let is_polymorphic_inductive_cumulativity =
@@ -847,19 +846,19 @@ let vernac_fixpoint_common ~atts discharge l =
 
 let vernac_fixpoint_interactive ~atts discharge l =
   let open DefAttributes in
-  let local = vernac_fixpoint_common ~atts discharge l in
+  let scope = vernac_fixpoint_common ~atts discharge l in
   if atts.program then
     CErrors.user_err Pp.(str"Program Fixpoint requires a body");
-  ComFixpoint.do_fixpoint_interactive local atts.polymorphic l
+  ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic l
 
 let vernac_fixpoint ~atts discharge l =
   let open DefAttributes in
-  let local = vernac_fixpoint_common ~atts discharge l in
+  let scope = vernac_fixpoint_common ~atts discharge l in
   if atts.program then
     (* XXX: Switch to the attribute system and match on ~atts *)
-    ComProgramFixpoint.do_fixpoint local atts.polymorphic l
+    ComProgramFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic l
   else
-    ComFixpoint.do_fixpoint local atts.polymorphic l
+    ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic l
 
 let vernac_cofixpoint_common ~atts discharge l =
   if Dumpglob.dump () then
@@ -868,18 +867,18 @@ let vernac_cofixpoint_common ~atts discharge l =
 
 let vernac_cofixpoint_interactive ~atts discharge l =
   let open DefAttributes in
-  let local = vernac_cofixpoint_common ~atts discharge l in
+  let scope = vernac_cofixpoint_common ~atts discharge l in
   if atts.program then
     CErrors.user_err Pp.(str"Program CoFixpoint requires a body");
-  ComFixpoint.do_cofixpoint_interactive local atts.polymorphic l
+  ComFixpoint.do_cofixpoint_interactive ~scope ~poly:atts.polymorphic l
 
 let vernac_cofixpoint ~atts discharge l =
   let open DefAttributes in
-  let local = vernac_cofixpoint_common ~atts discharge l in
+  let scope = vernac_cofixpoint_common ~atts discharge l in
   if atts.program then
-    ComProgramFixpoint.do_cofixpoint local atts.polymorphic l
+    ComProgramFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic l
   else
-    ComFixpoint.do_cofixpoint local atts.polymorphic l
+    ComFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic l
 
 let vernac_scheme l =
   if Dumpglob.dump () then