Merge PR #10316: [lemmas] Reify info for implicits, universe decls, and rec theorems.

Reviewed-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: gares
Reviewed-by: ppedrot

32 files changed, 625 insertions, 517 deletions

diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index 38852992e4..8b98408c5e 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -694,7 +694,7 @@ let make_bl_scheme mode mind =
   let ctx = UState.make (Global.universes ()) in
   let side_eff = side_effect_of_mode mode in
   let bl_goal = EConstr.of_constr bl_goal in
-  let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal
+  let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx bl_goal
     (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, EConstr.EInstance.empty) lnamesparrec nparrec)
   in
   ([|ans|], ctx), eff
@@ -824,7 +824,7 @@ let make_lb_scheme mode mind =
   let ctx = UState.make (Global.universes ()) in
   let side_eff = side_effect_of_mode mode in
   let lb_goal = EConstr.of_constr lb_goal in
-  let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal
+  let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx lb_goal
     (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)
   in
   ([|ans|], ctx), eff
@@ -1001,7 +1001,7 @@ let make_eq_decidability mode mind =
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let side_eff = side_effect_of_mode mode in
-  let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx
+  let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx
     (EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec))
     (compute_dec_tact ind lnamesparrec nparrec)
   in
diff --git a/vernac/class.ml b/vernac/class.ml
index d5c75ed809..febe8e34e4 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -338,42 +338,44 @@ let try_add_new_coercion_core ref ~local c d e f =
       user_err ~hdr:"try_add_new_coercion_core"
         (explain_coercion_error ref e ++ str ".")
 
-let try_add_new_coercion ref ~local poly =
+let try_add_new_coercion ref ~local ~poly =
   try_add_new_coercion_core ref ~local poly None None false
 
-let try_add_new_coercion_subclass cl ~local poly =
+let try_add_new_coercion_subclass cl ~local ~poly =
   let coe_ref = build_id_coercion None cl poly in
   try_add_new_coercion_core coe_ref ~local poly (Some cl) None true
 
-let try_add_new_coercion_with_target ref ~local poly ~source ~target =
+let try_add_new_coercion_with_target ref ~local ~poly ~source ~target =
   try_add_new_coercion_core ref ~local poly (Some source) (Some target) false
 
-let try_add_new_identity_coercion id ~local poly ~source ~target =
+let try_add_new_identity_coercion id ~local ~poly ~source ~target =
   let ref = build_id_coercion (Some id) source poly in
   try_add_new_coercion_core ref ~local poly (Some source) (Some target) true
 
-let try_add_new_coercion_with_source ref ~local poly ~source =
+let try_add_new_coercion_with_source ref ~local ~poly ~source =
   try_add_new_coercion_core ref ~local poly (Some source) None false
 
 let add_coercion_hook poly _uctx _trans local ref =
+  let open DeclareDef in
   let local = match local with
   | Discharge -> assert false (* Local Coercion in section behaves like Local Definition *)
   | Global ImportNeedQualified -> true
   | Global ImportDefaultBehavior -> false
   in
-  let () = try_add_new_coercion ref ~local poly in
+  let () = try_add_new_coercion ref ~local ~poly in
   let msg = Nametab.pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
   Flags.if_verbose Feedback.msg_info msg
 
-let add_coercion_hook poly = DeclareDef.Hook.make (add_coercion_hook poly)
+let add_coercion_hook ~poly = DeclareDef.Hook.make (add_coercion_hook poly)
 
-let add_subclass_hook poly _uctx _trans local ref =
+let add_subclass_hook ~poly _uctx _trans local ref =
+  let open DeclareDef in
   let stre = match local with
   | Discharge -> assert false (* Local Subclass in section behaves like Local Definition *)
   | Global ImportNeedQualified -> true
   | Global ImportDefaultBehavior -> false
   in
   let cl = class_of_global ref in
-  try_add_new_coercion_subclass cl ~local:stre poly
+  try_add_new_coercion_subclass cl ~local:stre ~poly
 
-let add_subclass_hook poly = DeclareDef.Hook.make (add_subclass_hook poly)
+let add_subclass_hook ~poly = DeclareDef.Hook.make (add_subclass_hook ~poly)
diff --git a/vernac/class.mli b/vernac/class.mli
index d530d218d4..3254d5d981 100644
--- a/vernac/class.mli
+++ b/vernac/class.mli
@@ -15,35 +15,39 @@ open Classops
 
 (** [try_add_new_coercion_with_target ref s src tg] declares [ref] as a coercion
    from [src] to [tg] *)
-val try_add_new_coercion_with_target : GlobRef.t -> local:bool ->
-  Decl_kinds.polymorphic ->
-  source:cl_typ -> target:cl_typ ->  unit
+val try_add_new_coercion_with_target
+  :  GlobRef.t
+  -> local:bool
+  -> poly:bool
+  -> source:cl_typ
+  -> target:cl_typ
+  -> unit
 
 (** [try_add_new_coercion ref s] declares [ref], assumed to be of type
    [(x1:T1)...(xn:Tn)src->tg], as a coercion from [src] to [tg] *)
-val try_add_new_coercion : GlobRef.t -> local:bool ->
-  Decl_kinds.polymorphic -> unit
+val try_add_new_coercion : GlobRef.t -> local:bool -> poly:bool -> unit
 
 (** [try_add_new_coercion_subclass cst s] expects that [cst] denotes a
    transparent constant which unfolds to some class [tg]; it declares
    an identity coercion from [cst] to [tg], named something like
    ["Id_cst_tg"] *)
-val try_add_new_coercion_subclass : cl_typ -> local:bool -> 
-  Decl_kinds.polymorphic -> unit
+val try_add_new_coercion_subclass : cl_typ -> local:bool -> poly:bool -> unit
 
 (** [try_add_new_coercion_with_source ref s src] declares [ref] as a coercion
    from [src] to [tg] where the target is inferred from the type of [ref] *)
 val try_add_new_coercion_with_source : GlobRef.t -> local:bool ->
-  Decl_kinds.polymorphic -> source:cl_typ -> unit
+  poly:bool -> source:cl_typ -> unit
 
 (** [try_add_new_identity_coercion id s src tg] enriches the
    environment with a new definition of name [id] declared as an
    identity coercion from [src] to [tg] *)
-val try_add_new_identity_coercion : Id.t -> local:bool -> 
-  Decl_kinds.polymorphic -> source:cl_typ -> target:cl_typ -> unit
+val try_add_new_identity_coercion
+  :  Id.t
+  -> local:bool
+  -> poly:bool -> source:cl_typ -> target:cl_typ -> unit
 
-val add_coercion_hook : Decl_kinds.polymorphic -> DeclareDef.Hook.t
+val add_coercion_hook : poly:bool -> DeclareDef.Hook.t
 
-val add_subclass_hook : Decl_kinds.polymorphic -> DeclareDef.Hook.t
+val add_subclass_hook : poly:bool -> DeclareDef.Hook.t
 
 val class_of_global : GlobRef.t -> cl_typ
diff --git a/vernac/classes.ml b/vernac/classes.ml
index d6a2f2727a..8addfa054e 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -362,21 +362,21 @@ 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:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly ~kind:Instance ~hook typ ctx obls)
 
-
-let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids term termtype =
+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
      the pretyping after the proof has opened. As a
      consequence, we use the low-level primitives to code
      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, poly, DefinitionBody Instance) in
-  let lemma = Lemmas.start_lemma id ~pl:decl kind sigma (EConstr.of_constr termtype)
-      ~hook:(DeclareDef.Hook.make
-               (fun _ _ _ -> instance_hook pri global imps ?hook)) in
+  let scope = DeclareDef.Global Declare.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 ~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
@@ -567,7 +567,7 @@ let new_instance_common ~program_mode ~generalize env instid ctx cl =
   id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl
 
 let new_instance_interactive ?(global=false)
-    poly instid ctx cl
+    ~poly instid ctx cl
     ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri =
   let env = Global.env() in
   let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
@@ -576,7 +576,7 @@ let new_instance_interactive ?(global=false)
     cty k u ctx ctx' pri decl imps subst id
 
 let new_instance_program ?(global=false)
-    poly instid ctx cl opt_props
+    ~poly instid ctx cl opt_props
     ?(generalize=true) ?hook pri =
   let env = Global.env() in
   let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
@@ -586,7 +586,7 @@ let new_instance_program ?(global=false)
   id
 
 let new_instance ?(global=false)
-    poly instid ctx cl props
+    ~poly instid ctx cl props
     ?(generalize=true) ?hook pri =
   let env = Global.env() in
   let id, env', sigma, k, u, cty, ctx', ctx, imps, subst, decl =
@@ -595,7 +595,7 @@ let new_instance ?(global=false)
     cty k u ctx ctx' pri decl imps subst id props;
   id
 
-let declare_new_instance ?(global=false) ~program_mode poly instid ctx cl pri =
+let declare_new_instance ?(global=false) ~program_mode ~poly instid ctx cl pri =
   let env = Global.env() in
   let ({CAst.loc;v=instid}, pl) = instid in
   let sigma, k, u, cty, ctx', ctx, imps, subst, decl =
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 472690cdd4..1247fdc8c1 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -27,7 +27,7 @@ val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit
 
 val new_instance_interactive
   :  ?global:bool (** Not global by default. *)
-  -> Decl_kinds.polymorphic
+  -> poly:bool
   -> name_decl
   -> local_binder_expr list
   -> constr_expr
@@ -39,7 +39,7 @@ val new_instance_interactive
 
 val new_instance
   :  ?global:bool (** Not global by default. *)
-  -> Decl_kinds.polymorphic
+  -> poly:bool
   -> name_decl
   -> local_binder_expr list
   -> constr_expr
@@ -51,7 +51,7 @@ val new_instance
 
 val new_instance_program
   : ?global:bool (** Not global by default. *)
-  -> Decl_kinds.polymorphic
+  -> poly:bool
   -> name_decl
   -> local_binder_expr list
   -> constr_expr
@@ -64,7 +64,7 @@ val new_instance_program
 val declare_new_instance
   : ?global:bool (** Not global by default. *)
   -> program_mode:bool
-  -> Decl_kinds.polymorphic
+  -> poly:bool
   -> ident_decl
   -> local_binder_expr list
   -> constr_expr
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index b0297b7c51..e791118db2 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -43,14 +43,15 @@ 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 typ univs pl imps impl nl {CAst.v=ident} =
+let open DeclareDef in
+match scope with
 | Discharge ->
-  let ctx = match ctx with
-    | Monomorphic_entry ctx -> ctx
-    | Polymorphic_entry (_, ctx) -> Univ.ContextSet.of_context ctx
+  let univs = match univs with
+    | Monomorphic_entry univs -> univs
+    | Polymorphic_entry (_, univs) -> Univ.ContextSet.of_context univs
   in
-  let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in
+  let decl = (Lib.cwd(), SectionLocalAssum {typ;univs;poly;impl}, IsAssumption kind) in
   let _ = declare_variable ident decl in
   let () = assumption_message ident in
   let r = VarRef ident in
@@ -58,7 +59,7 @@ match local with
   let env = Global.env () in
   let sigma = Evd.from_env env in
   let () = Classes.declare_instance env sigma None true r in
-  let () = if is_coe then Class.try_add_new_coercion r ~local:true false in
+  let () = if is_coe then Class.try_add_new_coercion r ~local:true ~poly:false in
   (r,Univ.Instance.empty,true)
 
 | Global local ->
@@ -68,7 +69,7 @@ match local with
     | DefaultInline -> Some (Flags.get_inline_level())
     | InlineAt i -> Some i
   in
-  let decl = (Declare.ParameterEntry (None,(c,ctx),inl), IsAssumption kind) in
+  let decl = (Declare.ParameterEntry (None,(typ,univs),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
@@ -78,9 +79,9 @@ 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 inst = match ctx with
-    | Polymorphic_entry (_, ctx) -> Univ.UContext.instance ctx
+  let () = if is_coe then Class.try_add_new_coercion gr ~local ~poly in
+  let inst = match univs with
+    | Polymorphic_entry (_, univs) -> Univ.UContext.instance univs
     | Monomorphic_entry _ -> Univ.Instance.empty
   in
     (gr,inst,Lib.is_modtype_strict ())
@@ -96,11 +97,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 typ 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 typ uctx pl imps false nl id in
       (ref',u')::refs, status' && status, next_uctx uctx)
       ([],true,uctx) idl
   in
@@ -115,7 +116,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 +124,9 @@ let process_assumptions_udecls kind l =
       udecl, id
     | (_, ([], _))::_ | [] -> assert false
   in
-  let () = match kind, udecl with
-    | (Discharge, _, _), Some _ ->
+  let open DeclareDef in
+  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 +134,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 +176,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
+  pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),typ,imps) ->
+      let typ = replace_vars subst typ in
+      let refs, status' = declare_assumptions idl is_coe ~poly ~scope ~kind typ uctx ubinders imps nl in
       let subst' = List.map2
           (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u)))
           idl refs
@@ -226,7 +228,7 @@ let named_of_rel_context l =
       l ([], [])
   in ctx
 
-let context poly l =
+let context ~poly l =
   let env = Global.env() in
   let sigma = Evd.from_env env in
   let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in
@@ -251,7 +253,7 @@ let context poly l =
            separately. *)
         begin
           let uctx = Evd.universe_context_set sigma in
-          Declare.declare_universe_context poly uctx;
+          Declare.declare_universe_context ~poly uctx;
           if poly then Polymorphic_entry ([||], Univ.UContext.empty)
           else Monomorphic_entry Univ.ContextSet.empty
         end
@@ -263,7 +265,7 @@ let context poly l =
            to avoid redeclaring them. *)
         begin
           let uctx = Evd.universe_context_set sigma in
-          Declare.declare_universe_context poly uctx;
+          Declare.declare_universe_context ~poly uctx;
           Monomorphic_entry Univ.ContextSet.empty
         end
   in
@@ -288,17 +290,17 @@ let context poly l =
       | _ -> false
       in
       let impl = List.exists test impls in
-      let persistence =
-        if Lib.sections_are_opened () then Discharge else Global ImportDefaultBehavior in
-      let decl = (persistence, poly, Context) in
+      let scope =
+        if Lib.sections_are_opened () then DeclareDef.Discharge else DeclareDef.Global ImportDefaultBehavior 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:DeclareDef.Discharge
+            ~kind:Definition UnivNames.empty_binders entry [] in
         Lib.sections_are_opened () || Lib.is_modtype_strict ()
       in
         status && nstatus
diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli
index 07e96d87a2..57b4aea9e3 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:bool
+  -> scope:DeclareDef.locality
+  -> kind:assumption_object_kind
   -> Declaremods.inline
   -> (ident_decl list * constr_expr) with_coercion list
   -> bool
@@ -26,8 +28,11 @@ val do_assumptions
     nor in a module type and meant to be instantiated. *)
 val declare_assumption
   : coercion_flag
-  -> assumption_kind
-  -> Constr.types Entries.in_universes_entry
+  -> poly:bool
+  -> scope:DeclareDef.locality
+  -> kind:assumption_object_kind
+  -> Constr.types
+  -> Entries.universes_entry
   -> UnivNames.universe_binders
   -> Impargs.manual_implicits
   -> bool (** implicit *)
@@ -40,7 +45,7 @@ val declare_assumption
 (** returns [false] if, for lack of section, it declares an assumption
     (unless in a module type). *)
 val context
-  : Decl_kinds.polymorphic
+  :  poly:bool
   -> local_binder_expr list
   -> bool
 
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index b3cc0a4236..57de719cb4 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -40,7 +40,7 @@ let check_imps ~impsty ~impsbody =
   | [], [] -> () in
   aux impsty impsbody
 
-let interp_definition ~program_mode pl bl poly red_option c ctypopt =
+let interp_definition ~program_mode pl bl ~poly red_option c ctypopt =
   let env = Global.env() in
   (* Explicitly bound universes and constraints *)
   let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in
@@ -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..71926a9d23 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:DeclareDef.locality
+  -> poly:bool
+  -> kind:definition_object_kind
   -> universe_decl_expr option
   -> local_binder_expr list
   -> red_expr option
@@ -36,7 +38,7 @@ val interp_definition
   :  program_mode:bool
   -> universe_decl_expr option
   -> local_binder_expr list
-  -> polymorphic
+  -> poly:bool
   -> red_expr option
   -> constr_expr
   -> constr_expr option
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index a88413cf7f..e3428d6afc 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -255,80 +255,59 @@ let interp_fixpoint ~cofix l ntns =
   let uctx,fix = ground_fixpoint env evd fix in
   (fix,pl,uctx,info)
 
-let declare_fixpoint_notations ntns =
-  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns
-
-let declare_fixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes ntns =
-  (* Some bodies to define by proof *)
+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, []
+  in
   let thms =
-    List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps))))
-              fixnames fixtypes fiximps in
+    List.map3 (fun name t (ctx,impargs,_) ->
+        { Lemmas.Recthm.name; typ = EConstr.of_constr t
+        ; args = List.map RelDecl.get_name ctx; impargs})
+      fixnames fixtypes fiximps in
   let init_tac =
-    Some (List.map (Option.cata (EConstr.of_constr %> Tactics.exact_no_check) Tacticals.New.tclIDTAC)
-      fixdefs) in
+    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 (local,poly,DefinitionBody Fixpoint)
-    evd pl (Some(false,indexes,init_tac)) thms None in
-  declare_fixpoint_notations ntns;
+  let lemma =
+    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 local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) indexes 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
+    | None -> [], true, CoFixpoint
+  in
   (* We shortcut the proof process *)
   let fixdefs = List.map Option.get fixdefs in
   let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
-  let env = Global.env() in
-  let indexes = search_guard env indexes fixdecls in
+  let vars, fixdecls, gidx =
+    if not cofix then
+      let env = Global.env() in
+      let indexes = search_guard env indexes fixdecls in
+      let vars = Vars.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
+      let fixdecls = List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
+      vars, fixdecls, Some indexes
+    else (* cofix *)
+      let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
+      let vars = Vars.universes_of_constr (List.hd fixdecls) in
+      vars, fixdecls, None
+  in
   let fiximps = List.map (fun (n,r,p) -> r) fiximps in
-  let vars = Vars.universes_of_constr (mkFix ((indexes,0),fixdecls)) in
-  let fixdecls =
-    List.map_i (fun i _ -> mkFix ((indexes,i),fixdecls)) 0 fixnames in
   let evd = Evd.from_ctx ctx in
   let evd = Evd.restrict_universe_context evd vars in
   let ctx = Evd.check_univ_decl ~poly evd pl in
   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, Fixpoint) pl ctx)
-            fixnames fixdecls fixtypes fiximps);
-  (* Declare the recursive definitions *)
-  fixpoint_message (Some indexes) fixnames;
-  declare_fixpoint_notations ntns
-
-let declare_cofixpoint_notations = declare_fixpoint_notations
-
-let declare_cofixpoint_interactive local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
-  (* Some bodies to define by proof *)
-  let thms =
-    List.map3 (fun id t (ctx,imps,_) -> (id,(EConstr.of_constr t,(List.map RelDecl.get_name ctx,imps))))
-              fixnames fixtypes fiximps in
-  let init_tac =
-    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
-    (Global ImportDefaultBehavior,poly, DefinitionBody CoFixpoint)
-    evd pl (Some(true,[],init_tac)) thms None in
-  declare_cofixpoint_notations ntns;
-  lemma
-
-let declare_cofixpoint local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx,fiximps) ntns =
-  (* We shortcut the proof process *)
-  let fixdefs = List.map Option.get fixdefs in
-  let fixdecls = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in
-  let fixdecls = List.map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 fixnames in
-  let vars = Vars.universes_of_constr (List.hd fixdecls) in
-  let mk_pure c = (c, Univ.ContextSet.empty), Evd.empty_side_effects in
-  let fixdecls = List.map mk_pure fixdecls in
-  let fiximps = List.map (fun (len,imps,idx) -> imps) fiximps in
-  let evd = Evd.from_ctx ctx in
-  let evd = Evd.restrict_universe_context evd vars in
-  let ctx = Evd.check_univ_decl ~poly evd pl in
-  let pl = Evd.universe_binders evd in
-  ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx)
+  ignore (List.map4 (fun name -> DeclareDef.declare_fix ~name ~scope ~kind:fix_kind pl ctx)
             fixnames fixdecls fixtypes fiximps);
-  (* Declare the recursive definitions *)
-  cofixpoint_message fixnames;
-  declare_cofixpoint_notations ntns
+  recursive_message (not cofix) gidx fixnames;
+  List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns;
+  ()
 
 let extract_decreasing_argument ~structonly = function { CAst.v = v } -> match v with
   | CStructRec na -> na
@@ -372,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 =
+let do_fixpoint_interactive ~scope ~poly l : Lemmas.t =
   let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in
-  let pstate = declare_fixpoint_interactive local poly fix possible_indexes 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 ();
-  pstate
+  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 local poly fix possible_indexes 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 pstate = declare_cofixpoint_interactive 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 ();
-  pstate
+  lemma
 
-let do_cofixpoint local poly l =
+let do_cofixpoint ~scope ~poly l =
   let ntns, cofix = do_cofixpoint_common l in
-  declare_cofixpoint 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 b42e877d41..982d316605 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -10,7 +10,6 @@
 
 open Names
 open Constr
-open Decl_kinds
 open Constrexpr
 open Vernacexpr
 
@@ -19,16 +18,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:DeclareDef.locality -> poly:bool -> (fixpoint_expr * decl_notation list) list -> Lemmas.t
 
 val do_fixpoint :
-  locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
+  scope:DeclareDef.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:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> Lemmas.t
 
 val do_cofixpoint :
-  locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
+  scope:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit
 
 (************************************************************************)
 (** Internal API  *)
@@ -81,22 +80,6 @@ val interp_fixpoint :
   recursive_preentry * UState.universe_decl * UState.t *
   (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
-(** Registering fixpoints and cofixpoints in the environment *)
-
-(** [Not used so far] *)
-val declare_fixpoint :
-  locality -> polymorphic ->
-  recursive_preentry * UState.universe_decl * UState.t *
-  (Constr.rel_context * Impargs.manual_implicits * int option) list ->
-  Lemmas.lemma_possible_guards -> decl_notation list ->
-  unit
-
-val declare_cofixpoint :
-  locality -> polymorphic ->
-  recursive_preentry * UState.universe_decl * UState.t *
-  (Constr.rel_context * Impargs.manual_implicits * int option) list ->
-  decl_notation list -> unit
-
 (** Very private function, do not use *)
 val compute_possible_guardness_evidences :
   ('a, 'b) Context.Rel.pt * 'c * int option -> int list
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 363ba5beff..f530dad4fd 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -349,7 +349,7 @@ let restrict_inductive_universes sigma ctx_params arities constructors =
   let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
   Evd.restrict_universe_context sigma uvars
 
-let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations cum poly prv finite =
+let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations cum ~poly prv finite =
   check_all_names_different indl;
   List.iter check_param paramsl;
   if not (List.is_empty uparamsl) && not (List.is_empty notations)
@@ -469,8 +469,8 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
       InferCumulativity.infer_inductive env_ar mind_ent
    else mind_ent), Evd.universe_binders sigma, impls
 
-let interp_mutual_inductive ~template udecl (paramsl,indl) notations cum poly prv finite =
-  interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations cum poly prv finite
+let interp_mutual_inductive ~template udecl (paramsl,indl) notations cum ~poly prv finite =
+  interp_mutual_inductive_gen (Global.env()) ~template udecl ([],paramsl,indl) notations cum ~poly prv finite
 
 (* Very syntactical equality *)
 let eq_local_binders bl1 bl2 =
@@ -564,16 +564,16 @@ type uniform_inductive_flag =
   | UniformParameters
   | NonUniformParameters
 
-let do_mutual_inductive ~template udecl indl cum poly prv ~uniform finite =
+let do_mutual_inductive ~template udecl indl cum ~poly prv ~uniform finite =
   let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in
   (* Interpret the types *)
   let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in
-  let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns cum poly prv finite in
+  let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns cum ~poly prv finite in
   (* Declare the mutual inductive block with its associated schemes *)
   ignore (declare_mutual_inductive_with_eliminations mie pl impls);
   (* Declare the possible notations of inductive types *)
   List.iter (Metasyntax.add_notation_interpretation (Global.env ())) ntns;
   (* Declare the coercions *)
-  List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false poly) coes;
+  List.iter (fun qid -> Class.try_add_new_coercion (Nametab.locate qid) ~local:false ~poly) coes;
   (* If positivity is assumed declares itself as unsafe. *)
   if Environ.deactivated_guard (Global.env ()) then Feedback.feedback Feedback.AddedAxiom else ()
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 2d6ecf48ef..a77cd66a33 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -26,7 +26,7 @@ type uniform_inductive_flag =
 val do_mutual_inductive :
   template:bool option -> universe_decl_expr option ->
   (one_inductive_expr * decl_notation list) list -> cumulative_inductive_flag ->
-  polymorphic -> private_flag -> uniform:uniform_inductive_flag ->
+  poly:bool -> private_flag -> uniform:uniform_inductive_flag ->
   Declarations.recursivity_kind -> unit
 
 (************************************************************************)
@@ -75,5 +75,5 @@ val extract_mutual_inductive_declaration_components :
 val interp_mutual_inductive :
   template:bool option -> universe_decl_expr option -> structured_inductive_expr ->
   decl_notation list -> cumulative_inductive_flag ->
-  polymorphic -> private_flag -> Declarations.recursivity_kind ->
+  poly:bool -> private_flag -> Declarations.recursivity_kind ->
   mutual_inductive_entry * UnivNames.universe_binders * one_inductive_impls list
diff --git a/vernac/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..f25abb95c3 100644
--- a/vernac/comProgramFixpoint.mli
+++ b/vernac/comProgramFixpoint.mli
@@ -1,12 +1,11 @@
-open Decl_kinds
 open Vernacexpr
 
 (** Special Fixpoint handling when command is activated. *)
 
 val do_fixpoint :
   (* When [false], assume guarded. *)
-  locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
+  scope:DeclareDef.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:DeclareDef.locality -> poly:bool -> (cofixpoint_expr * decl_notation list) list -> unit
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index a467c22ede..d74fdcab2c 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -13,12 +13,14 @@ open Declare
 open Globnames
 open Impargs
 
+type locality = Discharge | Global of Declare.import_status
+
 (* Hooks naturally belong here as they apply to both definitions and lemmas *)
 module Hook = struct
   module S = struct
     type t = UState.t
       -> (Names.Id.t * Constr.t) list
-      -> Decl_kinds.locality
+      -> locality
       -> Names.GlobRef.t
       -> unit
   end
@@ -36,31 +38,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..3934a29413 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -11,6 +11,8 @@
 open Names
 open Decl_kinds
 
+type locality = Discharge | Global of Declare.import_status
+
 (** Declaration hooks *)
 module Hook : sig
   type t
@@ -28,10 +30,10 @@ module Hook : sig
       (** [(n1,t1),...(nm,tm)]: association list between obligation
           name and the corresponding defined term (might be a constant,
           but also an arbitrary term in the Expand case of obligations) *)
-      -> Decl_kinds.locality
+      -> locality
       (**  [locality]: Locality of the original declaration *)
       -> GlobRef.t
-      (** [ref]: identifier of the origianl declaration *)
+      (** [ref]: identifier of the original declaration *)
       -> unit
   end
 
@@ -40,21 +42,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..81cde786c2 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 : DeclareDef.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, [||])
@@ -165,7 +167,7 @@ let declare_obligation prg obl body ty uctx =
     in
     (* ppedrot: seems legit to have obligations as local *)
     let constant =
-      Declare.declare_constant obl.obl_name ~local:ImportNeedQualified
+      Declare.declare_constant obl.obl_name ~local:Declare.ImportNeedQualified
         (Declare.DefinitionEntry ce, IsProof Property)
     in
     if not opaque then
@@ -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..2d275b5ed8 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 : DeclareDef.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 c2de83c1bb..173a83f1d1 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -56,13 +56,43 @@ module Proof_ending = struct
 
 end
 
+module Recthm = struct
+  type t =
+    { name : Id.t
+    ; typ : EConstr.t
+    ; args : Name.t list
+    ; impargs : Impargs.manual_implicits
+    }
+end
+
+module Info = struct
+
+  type t =
+    { hook : DeclareDef.Hook.t option
+    ; compute_guard : lemma_possible_guards
+    ; impargs : Impargs.manual_implicits
+    ; proof_ending : Proof_ending.t CEphemeron.key
+    (* This could be improved and the CEphemeron removed *)
+    ; other_thms : Recthm.t list
+    ; scope : DeclareDef.locality
+    ; kind : Decl_kinds.goal_object_kind
+    }
+
+  let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Proof Lemma) () =
+    { hook
+    ; compute_guard = []
+    ; impargs = []
+    ; proof_ending = CEphemeron.create proof_ending
+    ; other_thms = []
+    ; scope
+    ; kind
+    }
+end
+
 (* Proofs with a save constant function *)
 type t =
   { proof : Proof_global.t
-  ; hook : DeclareDef.Hook.t option
-  ; compute_guard : lemma_possible_guards
-  ; proof_ending : Proof_ending.t CEphemeron.key
-  (* This could be improved and the CEphemeron removed *)
+  ; info : Info.t
   }
 
 let pf_map f pf = { pf with proof = f pf.proof }
@@ -73,12 +103,11 @@ let set_endline_tactic t = pf_map (Proof_global.set_endline_tactic t)
 (* To be removed *)
 module Internal = struct
 
-(** Gets the current terminator without checking that the proof has
-    been completed. Useful for the likes of [Admitted]. *)
-let get_info ps = ps.hook, ps.compute_guard, ps.proof_ending
+  (** Gets the current terminator without checking that the proof has
+      been completed. Useful for the likes of [Admitted]. *)
+  let get_info ps = ps.info
 
 end
-(* Internal *)
 
 let by tac pf =
   let proof, res = Pfedit.by tac pf.proof in
@@ -114,15 +143,15 @@ let adjust_guardness_conditions const = function
           match Constr.kind body with
           | Fix ((nv,0),(_,_,fixdefs as fixdecls)) ->
 (*      let possible_indexes =
-	List.map2 (fun i c -> match i with Some i -> i | None ->
-	  List.interval 0 (List.length ((lam_assum c))))
-	  lemma_guard (Array.to_list fixdefs) in
+        List.map2 (fun i c -> match i with Some i -> i | None ->
+          List.interval 0 (List.length ((lam_assum c))))
+          lemma_guard (Array.to_list fixdefs) in
 *)
               let env = Safe_typing.push_private_constants env eff.Evd.seff_private in
               let indexes =
                 search_guard env
                   possible_indexes fixdecls in
-		(mkFix ((indexes,0),fixdecls), ctx), eff
+                (mkFix ((indexes,0),fixdecls), ctx), eff
           | _ -> (body, ctx), eff) }
 
 let find_mutually_recursive_statements sigma thms =
@@ -160,23 +189,23 @@ let find_mutually_recursive_statements sigma thms =
     (* (degenerated cartesian product since there is at most one coind ccl) *)
     let same_indccl =
       List.cartesians_filter (fun hyp oks ->
-	if List.for_all (of_same_mutind hyp) oks
-	then Some (hyp::oks) else None) [] ind_ccls in
+        if List.for_all (of_same_mutind hyp) oks
+        then Some (hyp::oks) else None) [] ind_ccls in
     let ordered_same_indccl =
       List.filter (List.for_all_i (fun i ((kn,j),_,_) -> Int.equal i j) 0) same_indccl in
     (* Check if some hypotheses are inductive in the same type *)
     let common_same_indhyp =
       List.cartesians_filter (fun hyp oks ->
-	if List.for_all (of_same_mutind hyp) oks
-	then Some (hyp::oks) else None) [] inds_hyps in
+        if List.for_all (of_same_mutind hyp) oks
+        then Some (hyp::oks) else None) [] inds_hyps in
     let ordered_inds,finite,guard =
       match ordered_same_indccl, common_same_indhyp with
       | indccl::rest, _ ->
-	  assert (List.is_empty rest);
+          assert (List.is_empty rest);
           (* One occ. of common coind ccls and no common inductive hyps *)
-	  if not (List.is_empty common_same_indhyp) then
-	    Flags.if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
-	  flush_all ();
+          if not (List.is_empty common_same_indhyp) then
+            Flags.if_verbose Feedback.msg_info (str "Assuming mutual coinductive statements.");
+          flush_all ();
           indccl, true, []
       | [], _::_ ->
           let () = match same_indccl with
@@ -191,10 +220,10 @@ let find_mutually_recursive_statements sigma thms =
           | _ -> ()
           in
           let possible_guards = List.map (List.map pi3) inds_hyps in
-	  (* assume the largest indices as possible *)
-	  List.last common_same_indhyp, false, possible_guards
+          (* assume the largest indices as possible *)
+          List.last common_same_indhyp, false, possible_guards
       | _, [] ->
-	  user_err Pp.(str
+        user_err Pp.(str
             ("Cannot find common (mutual) inductive premises or coinductive" ^
              " conclusions in the statements."))
     in
@@ -217,16 +246,18 @@ let default_thm_id = Id.of_string "Unnamed_thm"
 let check_name_freshness locality {CAst.loc;v=id} : unit =
   (* We check existence here: it's a bit late at Qed time *)
   if Nametab.exists_cci (Lib.make_path id) || is_section_variable id ||
-     locality <> Discharge && Nametab.exists_cci (Lib.make_path_except_section id)
+     locality <> DeclareDef.Discharge && Nametab.exists_cci (Lib.make_path_except_section id)
   then
     user_err ?loc  (Id.print id ++ str " already exists.")
 
-let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (id,(t_i,(_,imps))) =
-  let t_i = norm t_i in
+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
+    let open DeclareDef in
+      (match scope with
       | Discharge ->
           let impl = false in (* copy values from Vernacentries *)
           let univs = match univs with
@@ -235,17 +266,16 @@ let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (i
               Univ.ContextSet.of_context univs
             | Monomorphic_entry univs -> univs
           in
-          let c = SectionLocalAssum ((t_i, univs),p,impl) in
-	  let _ = declare_variable id (Lib.cwd(),c,k) in
-          (VarRef id,imps)
+          let c = SectionLocalAssum {typ=t_i;univs;poly;impl} in
+          let _ = declare_variable name (Lib.cwd(),c,k) in
+          (VarRef name,impargs)
       | Global local ->
           let k = IsAssumption Conjectural in
           let decl = (ParameterEntry (None,(t_i,univs),None), k) in
-          let kn = declare_constant id ~local decl in
-          (ConstRef kn,imps))
+          let kn = declare_constant name ~local decl in
+          (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)
@@ -255,18 +285,19 @@ let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (i
         | _ ->
           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
+      let open DeclareDef in
+      match scope with
       | Discharge ->
           let const = definition_entry ~types:t_i ~opaque:opaq ~univs body_i in
-	  let c = SectionLocalDef const in
-	  let _ = declare_variable id (Lib.cwd(), c, k) in
-          (VarRef id,imps)
+          let c = SectionLocalDef const in
+          let _ = declare_variable name (Lib.cwd(), c, k) in
+          (VarRef name,impargs)
       | Global local ->
         let const =
           Declare.definition_entry ~types:t_i ~univs ~opaque:opaq body_i
-	in
-        let kn = declare_constant id ~local (DefinitionEntry const, k) in
-        (ConstRef kn,imps)
+        in
+        let kn = declare_constant name ~local (DefinitionEntry const, k) in
+        (ConstRef kn,impargs)
 
 let initialize_named_context_for_proof () =
   let sign = Global.named_context () in
@@ -312,34 +343,38 @@ module Stack = struct
 end
 
 (* Starting a goal *)
-let start_lemma id ?pl kind sigma ?(proof_ending = Proof_ending.Regular)
-    ?(sign=initialize_named_context_for_proof()) ?(compute_guard=[]) ?hook c =
+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 id ?pl kind goals in
-  { proof ; hook; compute_guard; proof_ending = CEphemeron.create proof_ending }
+  let proof = Proof_global.start_proof sigma ~name ~udecl ~poly goals in
+  { proof ; info }
 
-let start_dependent_lemma id ?pl kind ?(proof_ending = Proof_ending.Regular)
-    ?(compute_guard=[]) ?hook telescope =
-  let proof = Proof_global.start_dependent_proof id ?pl kind telescope in
-  { proof; hook; compute_guard; proof_ending = CEphemeron.create proof_ending }
+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 telescope in
+  { proof; info }
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
-    match List.map (fun (id,(t,_)) -> (id,t)) thms with
+    match List.map (fun { Recthm.name; typ } -> name,typ) thms with
     | (id,_)::l -> Tactics.mutual_cofix id l 0
     | _ -> assert false
   else
     (* nl is dummy: it will be recomputed at Qed-time *)
-    let nl = match snl with 
+    let nl = match snl with
      | None -> List.map succ (List.map List.last guard)
      | Some nl -> nl
-    in match List.map2 (fun (id,(t,_)) n -> (id,n, t)) thms nl with
+    in match List.map2 (fun { Recthm.name; typ } n -> (name, n, typ)) thms nl with
        | (id,n,_)::l -> Tactics.mutual_fix id n l 0
        | _ -> assert false
 
-let start_lemma_with_initialization ?hook kind sigma decl recguard thms snl =
-  let intro_tac (_, (_, (ids, _))) = Tactics.auto_intros_tac ids in
-  let init_tac,guard = match recguard with
+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) ->
     let rec_tac = rec_tac_initializer finite guard thms snl in
     Some (match init_tac with
@@ -354,33 +389,26 @@ let start_lemma_with_initialization ?hook kind sigma decl recguard thms snl =
     Some (intro_tac (List.hd thms)), [] in
   match thms with
   | [] -> anomaly (Pp.str "No proof to start.")
-  | (id,(t,(_,imps)))::other_thms ->
-      let hook ctx _ strength ref =
-        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:(pi2 kind) ctx decl in
-            let env = Global.env () in
-            List.map_i (save_remaining_recthms env sigma kind 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 ?hook ctx [] strength ref) thms_data in
-      let hook = DeclareDef.Hook.make hook in
-      let lemma = start_lemma id ~pl:decl kind sigma t ~hook ~compute_guard:guard in
-      let lemma = 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 in
-      lemma
-
-let start_lemma_com ~program_mode ?inference_hook ?hook kind thms =
+  | { Recthm.name; typ; impargs; _}::other_thms ->
+    let info =
+      Info.{ hook
+           ; impargs
+           ; compute_guard
+           ; other_thms
+           ; proof_ending = CEphemeron.create Proof_ending.Regular
+           ; scope
+           ; kind
+           } 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 ~scope ~kind ?inference_hook ?hook thms =
   let env0 = Global.env () in
   let decl = fst (List.hd thms) in
-  let evd, decl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
+  let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
   let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) ->
     let evd, (impls, ((env, ctx), imps)) = interp_context_evars ~program_mode env0 evd bl in
     let evd, (t', imps') = interp_type_evars_impls ~program_mode ~impls env evd t in
@@ -388,7 +416,7 @@ let start_lemma_com ~program_mode ?inference_hook ?hook kind 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 (pi1 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),
@@ -398,18 +426,19 @@ let start_lemma_com ~program_mode ?inference_hook ?hook kind thms =
   let evd = Evd.minimize_universes evd in
   (* XXX: This nf_evar is critical too!! We are normalizing twice if
      you look at the previous lines... *)
-  let thms = List.map (fun (n, (t, info)) -> (n, (nf_evar evd t, info))) thms in
+  let thms = List.map (fun (name, (typ, (args, impargs))) ->
+      { Recthm.name; typ = nf_evar evd typ; args; impargs} ) thms in
   let () =
     let open UState in
-    if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then
-       ignore (Evd.check_univ_decl ~poly:(pi2 kind) evd decl)
+    if not (udecl.univdecl_extensible_instance && udecl.univdecl_extensible_constraints) then
+       ignore (Evd.check_univ_decl ~poly evd udecl)
   in
   let evd =
-    if pi2 kind then evd
+    if poly then evd
     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 kind evd decl recguard thms snl
+  start_lemma_with_initialization ?hook ~poly ~scope ~kind evd ~udecl recguard thms snl
 
 (************************************************************************)
 (* Admitting a lemma-like constant                                      *)
@@ -425,16 +454,21 @@ let warn_let_as_axiom =
                    (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++
                                 spc () ++ strbrk "declared as an axiom.")
 
-let finish_admitted id k pe ctx hook =
-  let local = match k with
-  | Global local, _, _ -> local
-  | Discharge, _, _ -> warn_let_as_axiom id; ImportNeedQualified
-  in
-  let kn = declare_constant id ~local (ParameterEntry pe, IsAssumption Conjectural) in
-  let () = assumption_message id in
-  Declare.declare_univ_binders (ConstRef kn) (UState.universe_binders ctx);
-  DeclareDef.Hook.call ?hook ctx [] (Global local) (ConstRef kn);
-  Feedback.feedback Feedback.AddedAxiom
+(* This declares implicits and calls the hooks for all the theorems,
+   including the main one *)
+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 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 [] scope ref) thms_data
 
 let get_keep_admitted_vars =
   Goptions.declare_bool_option_and_ref
@@ -443,22 +477,40 @@ let get_keep_admitted_vars =
     ~key:["Keep"; "Admitted"; "Variables"]
     ~value:true
 
+let finish_admitted env sigma ~name ~poly ~scope pe ctx hook ~udecl impargs other_thms =
+  let open DeclareDef in
+  let local = match scope with
+  | Global local -> local
+  | Discharge -> warn_let_as_axiom name; ImportNeedQualified
+  in
+  let kn = declare_constant name ~local (ParameterEntry pe, IsAssumption Conjectural) in
+  let () = assumption_message name 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 ~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 }, (hook, _, _)) ->
+    | Some ({ name; 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 } = List.hd entries in
+      let { proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
       if proof_entry_type = None then
         user_err Pp.(str "Admitted requires an explicit statement");
+      let poly = match proof_entry_universes with
+        | Entries.Monomorphic_entry _ -> false
+        | Entries.Polymorphic_entry (_, _) -> true in
       let typ = Option.get proof_entry_type in
-      let ctx = UState.univ_entry ~poly:(pi2 k) universes in
+      let ctx = UState.univ_entry ~poly universes in
       let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
-      finish_admitted id k (sec_vars, (typ, ctx), None) universes hook
+      let sigma = Evd.from_env env in
+      finish_admitted env sigma ~name ~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
@@ -467,7 +519,7 @@ let save_lemma_admitted ?proof ~(lemma : t) =
             ~label:"Lemmas.save_proof" (Pp.str "more than one statement.")
       in
       let typ = EConstr.Unsafe.to_constr typ in
-      let universes = Proof.((data pftree).initial_euctx) in
+      let universes = Proof_global.get_initial_euctx lemma.proof in
       (* This will warn if the proof is complete *)
       let pproofs, _univs =
         Proof_global.return_proof ~allow_partial:true lemma.proof in
@@ -481,46 +533,46 @@ let save_lemma_admitted ?proof ~(lemma : t) =
             let ids_def = Environ.global_vars_set env pproof in
             Some (Environ.keep_hyps env (Id.Set.union ids_typ ids_def))
           | _ -> None in
-      let decl = Proof_global.get_universe_decl lemma.proof in
-      let ctx = UState.check_univ_decl ~poly universes decl in
-      finish_admitted name gk (sec_vars, (typ, ctx), None) universes lemma.hook
+      let udecl = Proof_global.get_universe_decl lemma.proof in
+      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 ~poly ~scope (sec_vars, (typ, ctx), None) universes hook ~udecl impargs other_thms
 
 (************************************************************************)
 (* Saving a lemma-like constant                                         *)
 (************************************************************************)
 
-type proof_info = DeclareDef.Hook.t option * lemma_possible_guards * Proof_ending.t CEphemeron.key
-
-let default_info = None, [], CEphemeron.create Proof_ending.Regular
-
-let finish_proved opaque idopt po hook compute_guard =
+let finish_proved env sigma opaque idopt po info =
   let open Proof_global in
+  let { Info.hook; compute_guard; impargs; other_thms; scope; kind } = info in
   match po with
-  | { id; entries=[const]; persistence=locality,poly,kind; universes } ->
+  | { name; entries=[const]; universes; udecl; poly } ->
     let is_opaque = match opaque with
       | Transparent -> false
       | Opaque      -> true
     in
     assert (is_opaque == const.proof_entry_opaque);
-    let id = match idopt with
-      | None -> id
-      | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in
+    let name = match idopt with
+      | None -> name
+      | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in
     let fix_exn = Future.fix_exn_of const.proof_entry_body in
     let () = try
       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 open DeclareDef in
+      let r = match scope with
         | Discharge ->
           let c = SectionLocalDef const in
-          let _ = declare_variable id (Lib.cwd(), c, k) in
+          let _ = declare_variable name (Lib.cwd(), c, k) in
           let () = if should_suggest
-            then Proof_using.suggest_variable (Global.env ()) id
+            then Proof_using.suggest_variable (Global.env ()) name
           in
-          VarRef id
+          VarRef name
         | Global local ->
           let kn =
-            declare_constant id ~local (DefinitionEntry const, k) in
+            declare_constant name ~local (DefinitionEntry const, k) in
           let () = if should_suggest
             then Proof_using.suggest_constant (Global.env ()) kn
           in
@@ -528,8 +580,9 @@ let finish_proved opaque idopt po hook compute_guard =
           Declare.declare_univ_binders gr (UState.universe_binders universes);
           gr
       in
-      definition_message id;
-      DeclareDef.Hook.call ~fix_exn ?hook universes [] locality r
+      definition_message name;
+      (* This takes care of the implicits and hook for the current constant*)
+      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)
@@ -582,11 +635,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 pi3 proof_obj.Proof_global.persistence with
+  let kind = match kind with
     | DefinitionBody d -> IsDefinition d
     | Proof p -> IsProof p
   in
@@ -610,25 +663,28 @@ let save_lemma_proved ?proof ?lemma ~opaque ~idopt =
   (* Invariant (uh) *)
   if Option.is_empty lemma && Option.is_empty proof then
     user_err (str "No focused proof (No proof-editing in progress).");
-  let proof_obj, proof_info =
+  (* Env and sigma are just used for error printing in save_remaining_recthms *)
+  let env = Global.env () in
+  let sigma, proof_obj, proof_info =
     match proof with
     | None ->
       (* XXX: The close_proof and proof state API should be refactored
          so it is possible to insert proofs properly into the state *)
-      let { proof; hook; compute_guard; proof_ending } = Option.get lemma in
-      Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, (hook, compute_guard, proof_ending)
+      let { proof; info } = Option.get lemma in
+      let { Proof.sigma } = Proof.data (Proof_global.get_proof proof) in
+      sigma,
+      Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, info
     | Some (proof, info) ->
-      proof, info
+      Evd.from_env env, proof, info
   in
-  let hook, compute_guard, proof_ending = proof_info in
   let open Proof_global in
   let open Proof_ending in
-  match CEphemeron.default proof_ending Regular with
+  match CEphemeron.default proof_info.Info.proof_ending Regular with
   | Regular ->
-    finish_proved opaque idopt proof_obj hook compute_guard
+    finish_proved env sigma opaque idopt proof_obj proof_info
   | End_obligation oinfo ->
     DeclareObl.obligation_terminator opaque proof_obj.entries proof_obj.universes oinfo
   | 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 70c8b511a1..88f26a04b7 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -11,9 +11,11 @@
 open Names
 open Decl_kinds
 
-(* Proofs that define a constant *)
+(** {4 Proofs attached to a constant} *)
+
 type t
-type lemma_possible_guards = int list list
+(** [Lemmas.t] represents a constant that is being proved, usually
+    interactively *)
 
 module Stack : sig
 
@@ -40,11 +42,12 @@ end
 val set_endline_tactic : Genarg.glob_generic_argument -> t -> t
 val pf_map : (Proof_global.t -> Proof_global.t) -> t -> t
 val pf_fold : (Proof_global.t -> 'a) -> t -> 'a
+(** [pf_fold f l] fold over the underlying proof object *)
 
 val by : unit Proofview.tactic -> t -> t * bool
+(** [by tac l] apply a tactic to [l] *)
 
-(* Start of high-level proofs with an associated constant *)
-
+(** Creating high-level proofs with an associated constant *)
 module Proof_ending : sig
 
   type t =
@@ -60,71 +63,112 @@ module Proof_ending : sig
 
 end
 
+module Recthm : sig
+  type t =
+    { name : Id.t
+    (** Name of theorem *)
+    ; typ : EConstr.t
+    (** Type of theorem  *)
+    ; args : Name.t list
+    (** Names to pre-introduce  *)
+    ; impargs : Impargs.manual_implicits
+    (** Explicitily declared implicit arguments  *)
+    }
+end
+
+module Info : sig
+
+  type t
+
+  val make
+    :  ?hook: DeclareDef.Hook.t
+    (** Callback to be executed at the end of the proof *)
+    -> ?proof_ending : Proof_ending.t
+    (** Info for special constants *)
+    -> ?scope : DeclareDef.locality
+    (** locality  *)
+    -> ?kind:goal_object_kind
+    (** Theorem, etc... *)
+    -> unit
+    -> t
+
+end
+
+(** Starts the proof of a constant *)
 val start_lemma
-  :  Id.t
-  -> ?pl:UState.universe_decl
-  -> goal_kind
-  -> Evd.evar_map
-  -> ?proof_ending:Proof_ending.t
+  :  name:Id.t
+  -> poly:bool
+  -> ?udecl:UState.universe_decl
   -> ?sign:Environ.named_context_val
-  -> ?compute_guard:lemma_possible_guards
-  -> ?hook:DeclareDef.Hook.t
+  -> ?info:Info.t
+  -> Evd.evar_map
   -> EConstr.types
   -> t
 
 val start_dependent_lemma
-  :  Id.t
-  -> ?pl:UState.universe_decl
-  -> goal_kind
-  -> ?proof_ending:Proof_ending.t
-  -> ?compute_guard:lemma_possible_guards
-  -> ?hook:DeclareDef.Hook.t
+  :  name:Id.t
+  -> poly:bool
+  -> ?udecl:UState.universe_decl
+  -> ?info:Info.t
   -> Proofview.telescope
   -> t
 
-val start_lemma_com
-  :  program_mode:bool
-  -> ?inference_hook:Pretyping.inference_hook
-  -> ?hook:DeclareDef.Hook.t -> goal_kind -> Vernacexpr.proof_expr list
-  -> t
+type lemma_possible_guards = int list list
 
+(** Pretty much internal, only used in ComFixpoint *)
 val start_lemma_with_initialization
   :  ?hook:DeclareDef.Hook.t
-  -> goal_kind -> Evd.evar_map -> UState.universe_decl
+  -> poly:bool
+  -> scope:DeclareDef.locality
+  -> kind:goal_object_kind
+  -> udecl:UState.universe_decl
+  -> Evd.evar_map
   -> (bool * lemma_possible_guards * unit Proofview.tactic list option) option
-  -> (Id.t (* name of thm *) *
-     (EConstr.types (* type of thm *) *
-      (Name.t list (* names to pre-introduce *) * Impargs.manual_implicits))) list
+  -> Recthm.t list
   -> int list option
   -> t
 
 val default_thm_id : Names.Id.t
 
+(** Main [Lemma foo args : type.] command *)
+val start_lemma_com
+  :  program_mode:bool
+  -> poly:bool
+  -> scope:DeclareDef.locality
+  -> kind:goal_object_kind
+  -> ?inference_hook:Pretyping.inference_hook
+  -> ?hook:DeclareDef.Hook.t
+  -> Vernacexpr.proof_expr list
+  -> t
+
 (* Prepare global named context for proof session: remove proofs of
    opaque section definitions and remove vm-compiled code *)
 
 val initialize_named_context_for_proof : unit -> Environ.named_context_val
 
-(** {6 Saving proofs } *)
+(** {4 Saving proofs} *)
 
-type proof_info
+(** The extra [?proof] parameter here is due to problems with the
+    lower-level [Proof_global.close_proof] API; we cannot inject closed
+    proofs properly in the proof state so we must leave this backdoor open.
 
-val default_info : proof_info
+    The regular user can ignore it.
+*)
 
 val save_lemma_admitted
-  :  ?proof:(Proof_global.proof_object * proof_info)
+  :  ?proof:(Proof_global.proof_object * Info.t)
   -> lemma:t
   -> unit
 
 val save_lemma_proved
-  :  ?proof:(Proof_global.proof_object * proof_info)
+  :  ?proof:(Proof_global.proof_object * Info.t)
   -> ?lemma:t
   -> opaque:Proof_global.opacity_flag
   -> idopt:Names.lident option
   -> unit
 
-(* To be removed *)
+(** To be removed, don't use! *)
 module Internal : sig
+  val get_info : t -> Info.t
   (** Only needed due to the Proof_global compatibility layer. *)
-  val get_info : t -> proof_info
 end
diff --git a/vernac/locality.ml b/vernac/locality.ml
index bc33d53594..f033d32874 100644
--- a/vernac/locality.ml
+++ b/vernac/locality.ml
@@ -8,13 +8,11 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Decl_kinds
-
 (** * Managing locality *)
 
 let importability_of_bool = function
-  | true -> ImportNeedQualified
-  | false -> ImportDefaultBehavior
+  | true -> Declare.ImportNeedQualified
+  | false -> Declare.ImportDefaultBehavior
 
 (** Positioning locality for commands supporting discharging and export
      outside of modules *)
@@ -36,13 +34,15 @@ let warn_local_declaration =
         strbrk "available without qualification when imported.")
 
 let enforce_locality_exp locality_flag discharge =
+  let open DeclareDef in
+  let open Vernacexpr in
   match locality_flag, discharge with
   | Some b, NoDischarge -> Global (importability_of_bool b)
-  | None, NoDischarge -> Global ImportDefaultBehavior
+  | None, NoDischarge -> Global Declare.ImportDefaultBehavior
   | None, DoDischarge when not (Lib.sections_are_opened ()) ->
      (* If a Let/Variable is defined outside a section, then we consider it as a local definition *)
      warn_local_declaration ();
-     Global ImportNeedQualified
+     Global Declare.ImportNeedQualified
   | None, DoDischarge -> Discharge
   | Some true, DoDischarge -> CErrors.user_err Pp.(str "Local not allowed in this case")
   | Some false, DoDischarge -> CErrors.user_err Pp.(str "Global not allowed in this case")
diff --git a/vernac/locality.mli b/vernac/locality.mli
index be7e0cbe76..eda754324a 100644
--- a/vernac/locality.mli
+++ b/vernac/locality.mli
@@ -20,7 +20,7 @@
 
 val make_locality : bool option -> bool
 val make_non_locality : bool option -> bool
-val enforce_locality_exp : bool option -> Decl_kinds.discharge -> Decl_kinds.locality
+val enforce_locality_exp : bool option -> Vernacexpr.discharge -> DeclareDef.locality
 val enforce_locality : bool option -> bool
 
 (** For commands whose default is to not discharge but to export:
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index aa15718452..b7392a28ca 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
@@ -388,16 +398,14 @@ let deps_remaining obls deps =
     deps []
 
 
-let goal_kind poly =
-  Decl_kinds.(Global ImportNeedQualified, poly, DefinitionBody Definition)
+let goal_kind = DeclareDef.(Global Declare.ImportNeedQualified, DefinitionBody Definition)
+let goal_proof_kind = DeclareDef.(Global Declare.ImportNeedQualified, Proof Lemma)
 
-let goal_proof_kind poly =
-  Decl_kinds.(Global ImportNeedQualified, poly, Proof Lemma)
-
-let kind_of_obligation poly o =
+let kind_of_obligation o =
   match o with
-  | Evar_kinds.Define false | Evar_kinds.Expand -> goal_kind poly
-  | _ -> goal_proof_kind poly
+  | Evar_kinds.Define false
+  | Evar_kinds.Expand -> goal_kind
+  | _ -> goal_proof_kind
 
 let rec string_of_list sep f = function
     [] -> ""
@@ -410,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 ~goal_kind:(goal_kind poly) 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
@@ -445,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
@@ -486,13 +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 (pi2 prg.prg_kind) (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 lemma = Lemmas.start_lemma ~sign:prg.prg_sign obl.obl_name kind evd (EConstr.of_constr obl.obl_type) ~proof_ending ~hook 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=DeclareDef.Global Declare.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=DeclareDef.Global Declare.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 ->
@@ -680,7 +689,7 @@ let admit_prog prg =
         | None ->
             let x = subst_deps_obl obls x in
             let ctx = UState.univ_entry ~poly:false prg.prg_ctx in
-            let kn = Declare.declare_constant x.obl_name ~local:ImportNeedQualified
+            let kn = Declare.declare_constant x.obl_name ~local:Declare.ImportNeedQualified
               (Declare.ParameterEntry (None,(x.obl_type,ctx),None), IsAssumption Conjectural)
             in
               assumption_message x.obl_name;
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index a0010a5026..233739ee46 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:DeclareDef.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:DeclareDef.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/record.ml b/vernac/record.ml
index 9e3353bc54..268c778674 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -367,7 +367,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags f
 	    Impargs.maybe_declare_manual_implicits false refi impls;
             if flags.pf_subclass then begin
 	      let cl = Class.class_of_global (IndRef indsp) in
-	        Class.try_add_new_coercion_with_source refi ~local:false poly ~source:cl
+                Class.try_add_new_coercion_with_source refi ~local:false ~poly ~source:cl
 	    end;
 	    let i = if is_local_assum decl then i+1 else i in
 	      (Some kn::sp_projs, i, Projection term::subst)
@@ -470,7 +470,7 @@ let declare_structure ~cum finite ubinders univs paramimpls params template ?(ki
     let cstr = (rsp, 1) in
     let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
     let build = ConstructRef cstr in
-    let () = if is_coe then Class.try_add_new_coercion build ~local:false poly in
+    let () = if is_coe then Class.try_add_new_coercion build ~local:false ~poly in
     let () = declare_structure_entry (cstr, List.rev kinds, List.rev sp_projs) in
     rsp
   in
@@ -680,7 +680,7 @@ let extract_record_data records =
 (* [fs] corresponds to fields and [ps] to parameters; [coers] is a
    list telling if the corresponding fields must me declared as coercions
    or subinstances. *)
-let definition_structure udecl kind ~template cum poly finite records =
+let definition_structure udecl kind ~template cum ~poly finite records =
   let () = check_unique_names records in
   let () = check_priorities kind records in
   let ps, data = extract_record_data records in
diff --git a/vernac/record.mli b/vernac/record.mli
index 11d9a833e2..d0164572f3 100644
--- a/vernac/record.mli
+++ b/vernac/record.mli
@@ -31,15 +31,18 @@ val declare_projections :
 
 val declare_structure_entry : Recordops.struc_tuple -> unit
 
-val definition_structure :
-  universe_decl_expr option -> inductive_kind -> template:bool option ->
-  Decl_kinds.cumulative_inductive_flag -> Decl_kinds.polymorphic ->
-  Declarations.recursivity_kind ->
-  (coercion_flag *
-  Names.lident *
-  local_binder_expr list *
-  (local_decl_expr * record_field_attr) list *
-  Id.t * constr_expr option) list ->
-  GlobRef.t list
+val definition_structure
+  :  universe_decl_expr option
+  -> inductive_kind
+  -> template:bool option
+  -> Decl_kinds.cumulative_inductive_flag
+  -> poly:bool
+  -> Declarations.recursivity_kind
+  -> (coercion_flag *
+      Names.lident *
+      local_binder_expr list *
+      (local_decl_expr * record_field_attr) list *
+      Id.t * constr_expr option) list
+  -> GlobRef.t list
 
 val declare_existing_class : GlobRef.t -> unit
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 222f727f8e..dc46aad8af 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -560,7 +560,7 @@ let () =
 (***********)
 (* Gallina *)
 
-let start_proof_and_print ~program_mode ?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 =
@@ -574,7 +574,7 @@ let start_proof_and_print ~program_mode ?hook k l =
                   Evarutil.is_ground_term sigma concl)
           then raise Exit;
           let c, _, ctx =
-            Pfedit.build_by_tactic env (Evd.evar_universe_context sigma) concl tac
+            Pfedit.build_by_tactic ~poly:false env (Evd.evar_universe_context sigma) concl tac
           in Evd.set_universe_context sigma ctx, EConstr.of_constr c
         with Logic_monad.TacticFailure e when Logic.catchable_exception e ->
           user_err Pp.(str "The statement obligations could not be resolved \
@@ -582,15 +582,15 @@ let start_proof_and_print ~program_mode ?hook k l =
       in Some hook
     else None
   in
-  start_lemma_com ~program_mode ?inference_hook ?hook k l
+  start_lemma_com ~program_mode ?inference_hook ?hook ~poly ~scope ~kind l
 
-let vernac_definition_hook p = function
+let vernac_definition_hook ~poly = function
 | Coercion ->
-  Some (Class.add_coercion_hook p)
+  Some (Class.add_coercion_hook ~poly)
 | CanonicalStructure ->
   Some (DeclareDef.Hook.make (fun _ _ _ -> Canonical.declare_canonical_structure))
 | SubClass ->
-  Some (Class.add_subclass_hook p)
+  Some (Class.add_subclass_hook ~poly)
 | _ -> None
 
 let fresh_name_for_anonymous_theorem () =
@@ -603,6 +603,7 @@ let vernac_definition_name lid local =
          CAst.make ?loc (fresh_name_for_anonymous_theorem ())
     | { v = Name.Name n; loc } -> CAst.make ?loc n in
   let () =
+    let open DeclareDef in
     match local with
     | Discharge -> Dumpglob.dump_definition lid true "var"
     | Global _ -> Dumpglob.dump_definition lid false "def"
@@ -612,33 +613,34 @@ let vernac_definition_name lid local =
 let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t =
   let open DefAttributes in
   let local = enforce_locality_exp atts.locality discharge in
-  let hook = vernac_definition_hook atts.polymorphic kind in
+  let hook = vernac_definition_hook ~poly:atts.polymorphic kind in
   let program_mode = atts.program in
+  let poly = atts.polymorphic in
   let name = vernac_definition_name lid local in
-  start_proof_and_print ~program_mode (local, atts.polymorphic, 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 hook = vernac_definition_hook atts.polymorphic kind in
+  let scope = enforce_locality_exp atts.locality discharge in
+  let hook = vernac_definition_hook ~poly: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 (local, atts.polymorphic, 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 ->
@@ -665,15 +667,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
-            | 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
+          match scope with
+            | DeclareDef.Global _ -> Dumpglob.dump_definition lid false "ax"
+            | DeclareDef.Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
+  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 =
@@ -725,7 +726,7 @@ let vernac_record ~template udecl cum k poly finite records =
     coe, id, binders, cfs, const, sort
   in
   let records = List.map map records in
-  ignore(Record.definition_structure ~template udecl k is_cumulative poly finite records)
+  ignore(Record.definition_structure ~template udecl k is_cumulative ~poly finite records)
 
 let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) =
   match indl with
@@ -825,7 +826,7 @@ let vernac_inductive ~atts cum lo finite indl =
     let indl = List.map unpack indl in
     let is_cumulative = should_treat_as_cumulative cum poly in
     let uniform = should_treat_as_uniform () in
-    ComInductive.do_mutual_inductive ~template udecl indl is_cumulative poly lo ~uniform finite
+    ComInductive.do_mutual_inductive ~template udecl indl is_cumulative ~poly lo ~uniform finite
   else
     user_err (str "Mixed record-inductive definitions are not allowed")
 (*
@@ -846,19 +847,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
@@ -867,18 +868,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
@@ -901,14 +902,14 @@ let vernac_universe ~poly l =
     user_err ~hdr:"vernac_universe"
 		 (str"Polymorphic universes can only be declared inside sections, " ++
 		  str "use Monomorphic Universe instead");
-  Declare.do_universe poly l
+  Declare.do_universe ~poly l
 
 let vernac_constraint ~poly l =
   if poly && not (Lib.sections_are_opened ()) then
     user_err ~hdr:"vernac_constraint"
 		 (str"Polymorphic universe constraints can only be declared"
 		  ++ str " inside sections, use Monomorphic Constraint instead");
-  Declare.do_constraint poly l
+  Declare.do_constraint ~poly l
 
 (**********************)
 (* Modules            *)
@@ -1088,62 +1089,62 @@ let vernac_canonical r =
   Canonical.declare_canonical_structure (smart_global r)
 
 let vernac_coercion ~atts ref qids qidt =
-  let local, polymorphic = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
+  let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
   let local = enforce_locality local in
   let target = cl_of_qualid qidt in
   let source = cl_of_qualid qids in
   let ref' = smart_global ref in
-  Class.try_add_new_coercion_with_target ref' ~local polymorphic ~source ~target;
+  Class.try_add_new_coercion_with_target ref' ~local ~poly ~source ~target;
   Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion")
 
 let vernac_identity_coercion ~atts id qids qidt =
-  let local, polymorphic = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
+  let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
   let local = enforce_locality local in
   let target = cl_of_qualid qidt in
   let source = cl_of_qualid qids in
-  Class.try_add_new_identity_coercion id ~local polymorphic ~source ~target
+  Class.try_add_new_identity_coercion id ~local ~poly ~source ~target
 
 (* Type classes *)
 
 let vernac_instance_program ~atts name bl t props info =
   Dumpglob.dump_constraint (fst name) false "inst";
-  let (program, locality), polymorphic =
+  let (program, locality), poly =
     Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts
   in
   let global = not (make_section_locality locality) in
-  let _id : Id.t = Classes.new_instance_program ~global polymorphic name bl t props info in
+  let _id : Id.t = Classes.new_instance_program ~global ~poly name bl t props info in
   ()
 
 let vernac_instance_interactive ~atts name bl t info =
   Dumpglob.dump_constraint (fst name) false "inst";
-  let (program, locality), polymorphic =
+  let (program, locality), poly =
     Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts
   in
   let global = not (make_section_locality locality) in
   let _id, pstate =
-    Classes.new_instance_interactive ~global polymorphic name bl t info in
+    Classes.new_instance_interactive ~global ~poly name bl t info in
   pstate
 
 let vernac_instance ~atts name bl t props info =
   Dumpglob.dump_constraint (fst name) false "inst";
-  let (program, locality), polymorphic =
+  let (program, locality), poly =
     Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts
   in
   let global = not (make_section_locality locality) in
   let _id : Id.t =
-    Classes.new_instance ~global polymorphic name bl t props info in
+    Classes.new_instance ~global ~poly name bl t props info in
   ()
 
 let vernac_declare_instance ~atts id bl inst pri =
   Dumpglob.dump_definition (fst id) false "inst";
-  let (program, locality), polymorphic =
+  let (program, locality), poly =
     Attributes.(parse (Notations.(program ++ locality ++ polymorphic))) atts
   in
   let global = not (make_section_locality locality) in
-  Classes.declare_new_instance ~program_mode:program ~global polymorphic id bl inst pri
+  Classes.declare_new_instance ~program_mode:program ~global ~poly id bl inst pri
 
 let vernac_context ~poly l =
-  if not (ComAssumption.context poly l) then Feedback.feedback Feedback.AddedAxiom
+  if not (ComAssumption.context ~poly l) then Feedback.feedback Feedback.AddedAxiom
 
 let vernac_existing_instance ~section_local insts =
   let glob = not section_local in
@@ -1266,7 +1267,7 @@ let vernac_hints ~atts dbnames h =
   in
   let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
   let local = enforce_module_locality local in
-  Hints.add_hints ~local dbnames (Hints.interp_hints poly h)
+  Hints.add_hints ~local dbnames (Hints.interp_hints ~poly h)
 
 let vernac_syntactic_definition ~atts lid x compat =
   let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index e46212ca1c..ad3e9f93d9 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -22,7 +22,7 @@ val vernac_require :
 (** The main interpretation function of vernacular expressions *)
 val interp :
   ?verbosely:bool ->
-  ?proof:(Proof_global.proof_object * Lemmas.proof_info) ->
+  ?proof:(Proof_global.proof_object * Lemmas.Info.t) ->
   st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t
 
 (** Prepare a "match" template for a given inductive type.
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 6a67a49d0a..dc5df5904e 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -256,6 +256,8 @@ type extend_name =
      is given an offset, starting from zero. *)
   int
 
+type discharge = DoDischarge | NoDischarge
+
 type nonrec vernac_expr =
 
   | VernacLoad of verbose_flag * string
@@ -274,15 +276,15 @@ type nonrec vernac_expr =
   | VernacDeclareCustomEntry of string
 
   (* Gallina *)
-  | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr
+  | VernacDefinition of (discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr
   | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
-  | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) *
+  | VernacAssumption of (discharge * Decl_kinds.assumption_object_kind) *
       Declaremods.inline * (ident_decl list * constr_expr) with_coercion list
   | VernacInductive of vernac_cumulative option * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
-  | VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list
-  | VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list
+  | VernacFixpoint of discharge * (fixpoint_expr * decl_notation list) list
+  | VernacCoFixpoint of discharge * (cofixpoint_expr * decl_notation list) list
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
   | VernacUniverse of lident list
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 2bc20a747d..f9b4aec45e 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -131,7 +131,7 @@ module Proof_global = struct
       s_lemmas := Some stack;
       res
 
-  type closed_proof = Proof_global.proof_object * Lemmas.proof_info
+  type closed_proof = Proof_global.proof_object * Lemmas.Info.t
 
 
   let return_proof ?allow_partial () = cc (return_proof ?allow_partial)
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index 7e4d5d0315..5234ef7a73 100644
--- a/vernac/vernacstate.mli
+++ b/vernac/vernacstate.mli
@@ -51,7 +51,7 @@ module Proof_global : sig
 
   val return_proof : ?allow_partial:bool -> unit -> Proof_global.closed_proof_output
 
-  type closed_proof = Proof_global.proof_object * Lemmas.proof_info
+  type closed_proof = Proof_global.proof_object * Lemmas.Info.t
 
   val close_future_proof :
     opaque:Proof_global.opacity_flag ->