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

70 files changed, 993 insertions, 811 deletions

diff --git a/dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh b/dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh
new file mode 100644
index 0000000000..d133bc9993
--- /dev/null
+++ b/dev/ci/user-overlays/10316-ejgallego-proof+recthms.sh
@@ -0,0 +1,18 @@
+if [ "$CI_PULL_REQUEST" = "10316" ] || [ "$CI_BRANCH" = "proof+recthms" ]; then
+
+    elpi_CI_REF=proof+recthms
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+    equations_CI_REF=proof+recthms
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    mtac2_CI_REF=proof+recthms
+    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+    paramcoq_CI_REF=proof+recthms
+    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+    quickchick_CI_REF=proof+recthms
+    quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 51d90df89f..ab9df12766 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -13,13 +13,31 @@ Proof state:
 
   Proofs that are attached to a top-level constant (such as lemmas)
   are represented by `Lemmas.t`, as they do contain additional
-  information related to the constant declaration.
+  information related to the constant declaration. Some functions have
+  been renamed from `start_proof` to `start_lemma`
+
 
   Plugins that require access to the information about currently
   opened lemmas can add one of the `![proof]` attributes to their
   `mlg` entry, which will refine the type accordingly. See
   documentation in `vernacentries` for more information.
 
+  Proof `terminators` have been removed in favor of a principled
+  proof-saving path. This should not affect the regular API user, but
+  if plugin writes need special handling of the proof term they should
+  now work with Coq upstream to unsure the provided API does work and
+  is principled. Closing `hooks` are still available for simple
+  registration on constant save path, and essentially they do provide
+  the same power as terminators, but don't encourage their use other
+  than for simple tasks [such as adding a constant to a database]
+
+  Additionally, the API for proof/lemma handling has been refactored,
+  triples have been split into named arguments, and a few bits of
+  duplicated information among layers has been cleaned up. Most proof
+  information is now represented in a direct-style, as opposed to it
+  living inside closures in previous Coq versions; thus, proof
+  manipulation possibilities have been improved.
+
 ## Changes between Coq 8.9 and Coq 8.10
 
 ### ML4 Pre Processing
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index eb8161c2bb..68ae5628db 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,14 +1,12 @@
-let edeclare ?hook ident (_, poly, _ as k) ~opaque sigma udecl body tyopt imps =
+let edeclare ?hook ~name ~poly ~scope ~kind ~opaque sigma udecl body tyopt imps =
   let sigma, ce = DeclareDef.prepare_definition ~allow_evars:false
       ~opaque ~poly sigma udecl ~types:tyopt ~body in
   let uctx = Evd.evar_universe_context sigma in
   let ubinders = Evd.universe_binders sigma in
   let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
-  DeclareDef.declare_definition ident k ce ubinders imps ?hook_data
+  DeclareDef.declare_definition ~name ~scope ~kind ubinders ce imps ?hook_data
 
-let declare_definition ~poly ident sigma body =
-  let k = Decl_kinds.(Global ImportDefaultBehavior, poly, Definition) in
+let declare_definition ~poly name sigma body =
   let udecl = UState.default_univ_decl in
-  edeclare ident k ~opaque:false sigma udecl body None []
-
-(* But this definition cannot be undone by Reset ident *)
+  edeclare ~name ~poly ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+    ~kind:Decl_kinds.Definition ~opaque:false sigma udecl body None []
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 0e2ef95739..6eb582baef 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -10,16 +10,8 @@
 
 (** Informal mathematical status of declarations *)
 
-type discharge = DoDischarge | NoDischarge
-
-type import_status = ImportDefaultBehavior | ImportNeedQualified
-
-type locality = Discharge | Global of import_status
-
 type binding_kind = Explicit | Implicit
 
-type polymorphic = bool
-
 type private_flag = bool
 
 type cumulative_inductive_flag = bool
@@ -58,17 +50,12 @@ type assumption_object_kind = Definitional | Logical | Conjectural | Context
    Logical      |  Hypothesis | Axiom
 
 *)
-type assumption_kind = locality * polymorphic * assumption_object_kind
-type definition_kind = locality * polymorphic * definition_object_kind
-
 (** Kinds used in proofs *)
 
 type goal_object_kind =
   | DefinitionBody of definition_object_kind
   | Proof of theorem_kind
 
-type goal_kind = locality * polymorphic * goal_object_kind
-
 (** Kinds used in library *)
 
 type logical_kind =
diff --git a/library/decls.ml b/library/decls.ml
index ef60a44ac7..5cb35323dd 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -17,19 +17,24 @@ open Libnames
 
 (** Datas associated to section variables and local definitions *)
 
-type variable_data =
-  DirPath.t * bool (* opacity *) * Univ.ContextSet.t * polymorphic * logical_kind
+type variable_data = {
+  path:DirPath.t;
+  opaque:bool;
+  univs:Univ.ContextSet.t;
+  poly:bool;
+  kind:logical_kind;
+}
 
 let vartab =
   Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE"
 
 let add_variable_data id o = vartab := Id.Map.add id o !vartab
 
-let variable_path id = let (p,_,_,_,_) = Id.Map.find id !vartab in p
-let variable_opacity id = let (_,opaq,_,_,_) = Id.Map.find id !vartab in opaq
-let variable_kind id = let (_,_,_,_,k) = Id.Map.find id !vartab in k
-let variable_context id = let (_,_,ctx,_,_) = Id.Map.find id !vartab in ctx
-let variable_polymorphic id = let (_,_,_,p,_) = Id.Map.find id !vartab in p
+let variable_path id = let {path} = Id.Map.find id !vartab in path
+let variable_opacity id = let {opaque} = Id.Map.find id !vartab in opaque
+let variable_kind id = let {kind} = Id.Map.find id !vartab in kind
+let variable_context id = let {univs} = Id.Map.find id !vartab in univs
+let variable_polymorphic id = let {poly} = Id.Map.find id !vartab in poly
 
 let variable_secpath id =
   let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in
diff --git a/library/decls.mli b/library/decls.mli
index 0d09499b51..f88958bb04 100644
--- a/library/decls.mli
+++ b/library/decls.mli
@@ -18,8 +18,13 @@ open Decl_kinds
 
 (** Registration and access to the table of variable *)
 
-type variable_data =
-  DirPath.t * bool (* opacity *) * Univ.ContextSet.t * polymorphic * logical_kind
+type variable_data = {
+  path:DirPath.t;
+  opaque:bool;
+  univs:Univ.ContextSet.t;
+  poly:bool;
+  kind:logical_kind;
+}
 
 val add_variable_data : variable -> variable_data -> unit
 val variable_path : variable -> DirPath.t
@@ -27,7 +32,7 @@ val variable_secpath : variable -> qualid
 val variable_kind : variable -> logical_kind
 val variable_opacity : variable -> bool
 val variable_context : variable -> Univ.ContextSet.t
-val variable_polymorphic : variable -> polymorphic
+val variable_polymorphic : variable -> bool
 val variable_exists : variable -> bool
 
 (** Registration and access to the table of constants *)
diff --git a/library/lib.ml b/library/lib.ml
index ae657dbd70..3eb74808e4 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -411,8 +411,12 @@ type abstr_info = {
 type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
 
 type secentry =
-  | Variable of (Names.Id.t * Decl_kinds.binding_kind *
-		   Decl_kinds.polymorphic * Univ.ContextSet.t)
+  | Variable of {
+      id:Names.Id.t;
+      kind:Decl_kinds.binding_kind;
+      poly:bool;
+      univs:Univ.ContextSet.t;
+    }
   | Context of Univ.ContextSet.t
 
 let sectab =
@@ -424,16 +428,16 @@ let add_section () =
                 (Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab
 
 let check_same_poly p vars =
-  let pred = function Context _ -> p = false | Variable (_, _, poly, _) -> p != poly in
+  let pred = function Context _ -> p = false | Variable {poly} -> p != poly in
   if List.exists pred vars then
     user_err Pp.(str  "Cannot mix universe polymorphic and monomorphic declarations in sections.")
 
-let add_section_variable id impl poly ctx =
+let add_section_variable ~name ~kind ~poly univs =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | (vars,repl,abs)::sl ->
        List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab;
-       sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl
+       sectab := (Variable {id=name;kind;poly;univs}::vars,repl,abs)::sl
 
 let add_section_context ctx =
   match !sectab with
@@ -448,7 +452,7 @@ let is_polymorphic_univ u =
     let open Univ in
     List.iter (fun (vars,_,_) ->
         List.iter (function
-            | Variable (_,_,poly,(univs,_)) ->
+            | Variable {poly;univs=(univs,_)} ->
               if LSet.mem u univs then raise (PolyFound poly)
             | Context (univs,_) ->
               if LSet.mem u univs then raise (PolyFound true)
@@ -459,12 +463,12 @@ let is_polymorphic_univ u =
 
 let extract_hyps (secs,ohyps) =
   let rec aux = function
-    | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
+    | (Variable {id;kind;poly;univs}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
       let l, r = aux (idl,hyps) in 
-      (decl,impl) :: l, if poly then Univ.ContextSet.union r ctx else r
-    | (Variable (_,_,poly,ctx)::idl,hyps) ->
+      (decl,kind) :: l, if poly then Univ.ContextSet.union r univs else r
+    | (Variable {poly;univs}::idl,hyps) ->
         let l, r = aux (idl,hyps) in
-          l, if poly then Univ.ContextSet.union r ctx else r
+          l, if poly then Univ.ContextSet.union r univs else r
     | (Context ctx :: idl, hyps) ->
        let l, r = aux (idl, hyps) in
        l, Univ.ContextSet.union r ctx
@@ -509,11 +513,11 @@ let add_section_replacement f g poly hyps =
     } in
     sectab := (vars,f (inst,args) exps, g info abs) :: sl
 
-let add_section_kn poly kn =
+let add_section_kn ~poly kn =
   let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
     add_section_replacement f f poly
 
-let add_section_constant poly kn =
+let add_section_constant ~poly kn =
   let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
     add_section_replacement f f poly
 
@@ -543,7 +547,7 @@ let variable_section_segment_of_reference gr =
 let section_instance = function
   | VarRef id ->
      let eq = function
-       | Variable (id',_,_,_) -> Names.Id.equal id id'
+       | Variable {id=id'} -> Names.Id.equal id id'
        | Context _ -> false
      in
      if List.exists eq (pi1 (List.hd !sectab))
diff --git a/library/lib.mli b/library/lib.mli
index f6bd61e2da..2cd43b66b3 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -178,12 +178,10 @@ val variable_section_segment_of_reference : GlobRef.t -> variable_context
 val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array
 val is_in_section : GlobRef.t -> bool
 
-val add_section_variable : Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit
+val add_section_variable : name:Id.t -> kind:Decl_kinds.binding_kind -> poly:bool -> Univ.ContextSet.t -> unit
 val add_section_context : Univ.ContextSet.t -> unit
-val add_section_constant : Decl_kinds.polymorphic ->
-  Constant.t -> Constr.named_context -> unit
-val add_section_kn : Decl_kinds.polymorphic ->
-  MutInd.t -> Constr.named_context -> unit
+val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit
+val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit
 val replacement_context : unit -> Opaqueproof.work_list
 
 val is_polymorphic_univ : Univ.Level.t -> bool
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 72ca5dc8c4..e34150f2b3 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -19,7 +19,8 @@ let start_deriving f suchthat name : Lemmas.t =
 
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let kind = Decl_kinds.(Global ImportDefaultBehavior,false,DefinitionBody Definition) in
+  let poly = false in
+  let kind = Decl_kinds.(DefinitionBody Definition) in
 
   (* create a sort variable for the type of [f] *)
   (* spiwack: I don't know what the rigidity flag does, picked the one
@@ -39,8 +40,8 @@ let start_deriving f suchthat name : Lemmas.t =
                 TNil sigma))))))
   in
 
-  let proof_ending = Lemmas.Proof_ending.(End_derive {f; name}) in
-  let lemma = Lemmas.start_dependent_lemma name kind goals ~proof_ending in
+  let info = Lemmas.Info.make ~proof_ending:(Lemmas.Proof_ending.(End_derive {f; name})) ~kind () in
+  let lemma = Lemmas.start_dependent_lemma ~name ~poly ~info goals in
   Lemmas.pf_map (Proof_global.map_proof begin fun p ->
     Util.pi1 @@ Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
   end) lemma
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index ce3b5a82d6..a904b81d81 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -990,14 +990,19 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
       ]
   in
   (* Pp.msgnl (str "lemma type (2) " ++ Printer.pr_lconstr_env (Global.env ()) evd lemma_type); *)
+  let info = Lemmas.Info.make
+      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+      ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in
+
   let lemma = Lemmas.start_lemma
     (*i The next call to mk_equation_id is valid since we are constructing the lemma
       Ensures by: obvious
       i*)
-    (mk_equation_id f_id)
-    Decl_kinds.(Global ImportDefaultBehavior, false, Proof Theorem)
-    evd
-  lemma_type
+      ~name:(mk_equation_id f_id)
+      ~poly:false
+      ~info
+      evd
+      lemma_type
   in
   let lemma,_ = Lemmas.by (Proofview.V82.tactic prove_replacement) lemma in
   let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index d49d657d38..edda2f2eef 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -309,8 +309,8 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   let hook = DeclareDef.Hook.make (hook new_principle_type) in
   let lemma =
     Lemmas.start_lemma
-      new_princ_name
-      Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
+      ~name:new_princ_name
+      ~poly:false
       !evd
       (EConstr.of_constr new_principle_type)
   in
@@ -324,10 +324,10 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   (*    end; *)
 
   let open Proof_global in
-  let { id; entries; persistence } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in
+  let { name; entries } = Lemmas.pf_fold (close_proof ~opaque:Transparent ~keep_body_ucst_separate:false (fun x -> x)) lemma in
   match entries with
   | [entry] ->
-    (id,(entry,persistence)), hook
+    name, entry, hook
   | _ ->
     CErrors.anomaly Pp.(str "[build_functional_principle] close_proof returned more than one proof term")
 
@@ -379,7 +379,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
       register_with_sort InProp;
       register_with_sort InSet
   in
-  let ((id,(entry,g_kind)),hook) =
+  let id,entry,hook =
     build_functional_principle evd interactive_proof old_princ_type new_sorts funs i
     proof_tac hook
   in
@@ -387,7 +387,7 @@ let generate_functional_principle (evd: Evd.evar_map ref)
      Don't forget to close the goal if an error is raised !!!!
   *)
   let uctx = Evd.evar_universe_context sigma in
-  save new_princ_name entry ~hook uctx g_kind
+  save new_princ_name entry ~hook uctx (DeclareDef.Global Declare.ImportDefaultBehavior) Decl_kinds.(Proof Theorem)
   with e when CErrors.noncritical e ->
     raise (Defining_principle e)
 
@@ -518,7 +518,7 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects Pro
         s::l_schemes -> s,l_schemes
       | _ -> anomaly (Pp.str "")
   in
-  let ((_,(const,_)),_) =
+  let _,const,_ =
     try
       build_functional_principle evd false
         first_type
@@ -576,10 +576,10 @@ let make_scheme evd (fas : (pconstant*Sorts.family) list) : Evd.side_effects Pro
 
              )
              ta;
-           (* If we reach this point, the two principle are not mutually recursive
-              We fall back to the previous method
-           *)
-             let ((_,(const,_)),_) =
+             (* If we reach this point, the two principle are not mutually recursive
+                We fall back to the previous method
+                *)
+             let _,const,_ =
                build_functional_principle
                  evd
                  false
diff --git a/plugins/funind/g_indfun.mlg b/plugins/funind/g_indfun.mlg
index ef9d91c7fa..e20d010c71 100644
--- a/plugins/funind/g_indfun.mlg
+++ b/plugins/funind/g_indfun.mlg
@@ -182,7 +182,7 @@ let is_proof_termination_interactively_checked recsl =
 
 let classify_as_Fixpoint recsl =
  Vernac_classifier.classify_vernac
-    (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl))))
+    (Vernacexpr.(CAst.make @@ VernacExpr([], VernacFixpoint(NoDischarge, List.map snd recsl))))
 
 let classify_funind recsl =
   match classify_as_Fixpoint recsl with
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 201d953692..bb4e745fe9 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1506,7 +1506,7 @@ let do_build_inductive
   let _time2 = System.get_time () in
   try
     with_full_print
-      (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds false false false ~uniform:ComInductive.NonUniformParameters))
+      (Flags.silently (ComInductive.do_mutual_inductive ~template:(Some false) None rel_inds false ~poly:false false ~uniform:ComInductive.NonUniformParameters))
       Declarations.Finite
   with
     | UserError(s,msg) as e ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 0ecfbacb09..d305a58ccc 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -416,8 +416,10 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
       let body = match body with | Some body -> body | None -> user_err ~hdr:"Function" (str "Body of Function must be given") in
       ComDefinition.do_definition
         ~program_mode:false
-        fname
-        Decl_kinds.(Global ImportDefaultBehavior,false,Definition) pl
+        ~name:fname
+        ~poly:false
+        ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+        ~kind:Decl_kinds.Definition pl
         bl None body (Some ret_type);
        let evd,rev_pconstants =
          List.fold_left
@@ -434,7 +436,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        in
        None, evd,List.rev rev_pconstants
     | _ ->
-       ComFixpoint.do_fixpoint (Global ImportDefaultBehavior) false fixpoint_exprl;
+       ComFixpoint.do_fixpoint ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~poly:false fixpoint_exprl;
        let evd,rev_pconstants =
          List.fold_left
            (fun (evd,l) ((({CAst.v=fname},_),_,_,_,_),_) ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 17c79e0e6c..254760cb50 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -118,12 +118,12 @@ let refl_equal = lazy(EConstr.of_constr (coq_constant "eq_refl"))
 (* Copy of the standard save mechanism but without the much too  *)
 (* slow reduction function                                       *)
 (*****************************************************************)
-open Decl_kinds
 open Declare
+open DeclareDef
 
 let definition_message = Declare.definition_message
 
-let save id const ?hook uctx (locality,_,kind) =
+let save id const ?hook uctx locality kind =
   let fix_exn = Future.fix_exn_of const.Proof_global.proof_entry_body in
   let r = match locality with
     | Discharge ->
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 1d096fa488..45d332031f 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -47,7 +47,8 @@ val save
   -> Evd.side_effects Proof_global.proof_entry
   -> ?hook:DeclareDef.Hook.t
   -> UState.t
-  -> Decl_kinds.goal_kind
+  -> DeclareDef.locality
+  -> Decl_kinds.goal_object_kind
   -> unit
 
 (* [with_full_print f a] applies [f] to [a] in full printing environment.
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 2020881c7c..587e1fc2e8 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -803,11 +803,15 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
          i*)
          let lem_id = mk_correct_id f_id in
          let (typ,_) = lemmas_types_infos.(i) in
+         let info = Lemmas.Info.make
+             ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+             ~kind:(Decl_kinds.Proof Decl_kinds.Theorem) () in
          let lemma = Lemmas.start_lemma
-           lem_id
-           Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem)
-           !evd
-           typ in
+             ~name:lem_id
+             ~poly:false
+             ~info
+             !evd
+             typ in
          let lemma = fst @@ Lemmas.by
                    (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
                                                       (proving_tac i))) lemma in
@@ -865,12 +869,14 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
              Ensures by: obvious
            i*)
          let lem_id = mk_complete_id f_id in
-         let lemma = Lemmas.start_lemma lem_id
-           Decl_kinds.(Global ImportDefaultBehavior,false,Proof Theorem) sigma
-         (fst lemmas_types_infos.(i)) in
+         let info = Lemmas.Info.make
+             ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
+             ~kind:Decl_kinds.(Proof Theorem) () in
+         let lemma = Lemmas.start_lemma ~name:lem_id ~poly:false ~info
+             sigma (fst lemmas_types_infos.(i)) in
          let lemma = fst (Lemmas.by
-           (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
-              (proving_tac i))) lemma) in
+                            (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
+                                                     (proving_tac i))) lemma) in
          let () = Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:Proof_global.Transparent ~idopt:None in
          let finfo = find_Function_infos (fst f_as_constant) in
          let _,lem_cst_constr = Evd.fresh_global
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 2647e7449b..425e498330 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1367,10 +1367,13 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
     in
     Lemmas.save_lemma_proved ?proof:None ~lemma ~opaque:opacity ~idopt:None
   in
+  let info = Lemmas.Info.make ~hook:(DeclareDef.Hook.make hook)
+      ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior) ~kind:(Decl_kinds.Proof Decl_kinds.Lemma)
+      () in
   let lemma = Lemmas.start_lemma
-    na
-    Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma)
-    sigma gls_type ~hook:(DeclareDef.Hook.make hook) in
+      ~name:na
+      ~poly:false (* FIXME *) ~info
+      sigma gls_type in
   let lemma = if Indfun_common.is_strict_tcc  ()
   then
     fst @@ Lemmas.by (Proofview.V82.tactic (tclIDTAC)) lemma
@@ -1408,9 +1411,13 @@ let com_terminate
     nb_args ctx
     hook =
   let start_proof env ctx (tac_start:tactic) (tac_end:tactic) =
-    let lemma = Lemmas.start_lemma thm_name
-      (Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma) ~sign:(Environ.named_context_val env)
-      ctx (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) ~hook in
+    let info = Lemmas.Info.make ~hook ~scope:(DeclareDef.Global ImportDefaultBehavior) ~kind:(Proof Lemma) () in
+    let lemma = Lemmas.start_lemma ~name:thm_name
+        ~poly:false (*FIXME*)
+        ~sign:(Environ.named_context_val env)
+        ~info
+        ctx
+        (EConstr.of_constr (compute_terminate_type nb_args fonctional_ref)) in
     let lemma = fst @@ Lemmas.by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "starting_tac") tac_start)) lemma in
     fst @@ Lemmas.by (Proofview.V82.tactic (observe_tac (fun _ _ -> str "whole_start") (whole_start tac_end nb_args is_mes fonctional_ref
                                    input_type relation rec_arg_num ))) lemma
@@ -1455,7 +1462,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
     let evd = Evd.from_ctx uctx in
     let f_constr = constr_of_monomorphic_global f_ref in
     let equation_lemma_type = subst1 f_constr equation_lemma_type in
-    let lemma = Lemmas.start_lemma eq_name (Global ImportDefaultBehavior, false, Proof Lemma) ~sign evd
+    let lemma = Lemmas.start_lemma ~name:eq_name ~poly:false ~sign evd
        (EConstr.of_constr equation_lemma_type) in
     let lemma = fst @@ Lemmas.by
        (Proofview.V82.tactic (start_equation f_ref terminate_ref
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 49d8ab4e23..1e2b23bf96 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -328,7 +328,7 @@ let add_rewrite_hint ~poly bases ort t lcsr =
         if poly then ctx
 	else (* This is a global universe context that shouldn't be
 	        refreshed at every use of the hint, declare it globally. *)
-	  (Declare.declare_universe_context false ctx;
+          (Declare.declare_universe_context ~poly:false ctx;
            Univ.ContextSet.empty)
     in
       CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index f977ba34d2..9d928232c6 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1795,7 +1795,7 @@ let declare_an_instance n s args =
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
 let anew_instance atts binders (name,t) fields =
-  let _id = Classes.new_instance atts.polymorphic
+  let _id = Classes.new_instance ~poly:atts.polymorphic
       name binders t (true, CAst.make @@ CRecord (fields))
       ~global:atts.global ~generalize:false Hints.empty_hint_info
   in
@@ -1994,9 +1994,8 @@ let add_morphism_interactive atts m n : Lemmas.t =
   let env = Global.env () in
   let evd = Evd.from_env env in
   let uctx, instance = build_morphism_signature env evd m in
-  let kind = Decl_kinds.Global Decl_kinds.ImportDefaultBehavior, atts.polymorphic,
-             Decl_kinds.DefinitionBody Decl_kinds.Instance
-  in
+  let poly = atts.polymorphic in
+  let kind = Decl_kinds.DefinitionBody Decl_kinds.Instance in
   let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
   let hook _ _ _ = function
     | Globnames.ConstRef cst ->
@@ -2007,9 +2006,10 @@ let add_morphism_interactive atts m n : Lemmas.t =
     | _ -> assert false
   in
   let hook = DeclareDef.Hook.make hook in
+  let info = Lemmas.Info.make ~hook ~kind () in
   Flags.silently
     (fun () ->
-       let lemma = Lemmas.start_lemma ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+       let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in
        fst (Lemmas.by (Tacinterp.interp tac) lemma)) ()
 
 let add_morphism atts binders m s n =
@@ -2023,7 +2023,7 @@ let add_morphism atts binders m s n =
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
   let _id, lemma = Classes.new_instance_interactive
-      ~global:atts.global atts.polymorphic
+      ~global:atts.global ~poly:atts.polymorphic
       instance_name binders instance_t
       ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info
   in
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 9bbe339770..33798c43c8 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -153,7 +153,7 @@ let decl_constant na univs c =
   let open Constr in
   let vars = CVars.universes_of_constr c in
   let univs = UState.restrict_universe_context univs vars in
-  let () = Declare.declare_universe_context false univs in
+  let () = Declare.declare_universe_context ~poly:false univs in
   let types = (Typeops.infer (Global.env ()) c).uj_type in
   let univs = Monomorphic_entry Univ.ContextSet.empty in
   mkConst(declare_constant (Id.of_string na) 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index cb4eabcc85..ed60b8274a 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -112,14 +112,12 @@ let by tac = Proof_global.map_fold_proof (solve (Goal_select.SelectNth 1) None t
 (**********************************************************************)
 (* Shortcut to build a term using tactics *)
 
-open Decl_kinds
-
 let next = let n = ref 0 in fun () -> incr n; !n
 
-let build_constant_by_tactic id ctx sign ?(goal_kind = Global ImportDefaultBehavior, false, Proof Theorem) typ tac =
+let build_constant_by_tactic ~name ctx sign ~poly typ tac =
   let evd = Evd.from_ctx ctx in
   let goals = [ (Global.env_of_context sign , typ) ] in
-  let pf = Proof_global.start_proof evd id goal_kind goals in
+  let pf = Proof_global.start_proof ~name ~poly ~udecl:UState.default_univ_decl evd goals in
   try
     let pf, status = by tac pf in
     let open Proof_global in
@@ -134,12 +132,10 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global ImportDefaultBehav
     let reraise = CErrors.push reraise in
     iraise reraise
 
-let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
-  let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
+let build_by_tactic ?(side_eff=true) env sigma ~poly typ tac =
+  let name = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
-  let gk = Global ImportDefaultBehavior, poly, Proof Theorem in
-  let ce, status, univs =
-    build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in
+  let ce, status, univs = build_constant_by_tactic ~name sigma sign ~poly typ tac in
   let body, eff = Future.force ce.Proof_global.proof_entry_body in
   let (cb, ctx) =
     if side_eff then Safe_typing.inline_private_constants env (body, eff.Evd.seff_private)
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index d01704926a..0626e40047 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -13,7 +13,6 @@
 open Names
 open Constr
 open Environ
-open Decl_kinds
 
 (** {6 ... } *)
 
@@ -58,15 +57,23 @@ val use_unification_heuristics : unit -> bool
     [tac]. The return boolean, if [false] indicates the use of an unsafe
     tactic. *)
 
-val build_constant_by_tactic :
-  Id.t -> UState.t -> named_context_val -> ?goal_kind:goal_kind ->
-  EConstr.types -> unit Proofview.tactic -> 
-  Evd.side_effects Proof_global.proof_entry * bool *
-    UState.t
+val build_constant_by_tactic
+  :  name:Id.t
+  -> UState.t
+  -> named_context_val
+  -> poly:bool
+  -> EConstr.types
+  -> unit Proofview.tactic
+  -> Evd.side_effects Proof_global.proof_entry * bool * UState.t
 
-val build_by_tactic : ?side_eff:bool -> env -> UState.t -> ?poly:polymorphic ->
-  EConstr.types -> unit Proofview.tactic -> 
-  constr * bool * UState.t
+val build_by_tactic
+  :  ?side_eff:bool
+  -> env
+  -> UState.t
+  -> poly:bool
+  -> EConstr.types
+  -> unit Proofview.tactic
+  -> constr * bool * UState.t
 
 val refine_by_tactic
   :  name:Id.t
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 47502fe402..9f2c90c375 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -118,8 +118,6 @@ type t =
   (** List of goals that have been shelved. *)
   ; given_up : Goal.goal list
   (** List of goals that have been given up *)
-  ; initial_euctx : UState.t
-  (** The initial universe context (for the statement) *)
   ; name : Names.Id.t
   (** the name of the theorem whose proof is being constructed *)
   ; poly : bool
@@ -290,14 +288,12 @@ let unfocused = is_last_focus end_of_stack_kind
 
 let start ~name ~poly sigma goals =
   let entry, proofview = Proofview.init sigma goals in
-  let pr = {
-    proofview;
-    entry;
-    focus_stack = [] ;
-    shelf = [] ;
-    given_up = [];
-    initial_euctx =
-      Evd.evar_universe_context (snd (Proofview.proofview proofview))
+  let pr =
+    { proofview
+    ; entry
+    ; focus_stack = []
+    ; shelf = []
+    ; given_up = []
     ; name
     ; poly
   } in
@@ -305,14 +301,12 @@ let start ~name ~poly sigma goals =
 
 let dependent_start ~name ~poly goals =
   let entry, proofview = Proofview.dependent_init goals in
-  let pr = {
-    proofview;
-    entry;
-    focus_stack = [] ;
-    shelf = [] ;
-    given_up = [];
-    initial_euctx =
-      Evd.evar_universe_context (snd (Proofview.proofview proofview))
+  let pr =
+    { proofview
+    ; entry
+    ; focus_stack = []
+    ; shelf = []
+    ; given_up = []
     ; name
     ; poly
   } in
@@ -488,15 +482,13 @@ type data =
   (** A representation of the shelf  *)
   ; given_up : Evar.t list
   (** A representation of the given up goals  *)
-  ; initial_euctx : UState.t
-  (** The initial universe context (for the statement) *)
   ; name : Names.Id.t
   (** The name of the theorem whose proof is being constructed *)
   ; poly : bool
   (** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *)
   }
 
-let data { proofview; focus_stack; entry; shelf; given_up; initial_euctx; name; poly } =
+let data { proofview; focus_stack; entry; shelf; given_up; name; poly } =
   let goals, sigma = Proofview.proofview proofview in
   (* spiwack: beware, the bottom of the stack is used by [Proof]
      internally, and should not be exposed. *)
@@ -507,7 +499,7 @@ let data { proofview; focus_stack; entry; shelf; given_up; initial_euctx; name;
   in
   let stack =
     map_minus_one (fun (_,_,c) -> Proofview.focus_context c) focus_stack in
-  { sigma; goals; entry; stack; shelf; given_up; initial_euctx; name; poly }
+  { sigma; goals; entry; stack; shelf; given_up; name; poly }
 
 let pr_proof p =
   let { goals=fg_goals; stack=bg_goals; shelf; given_up; _ } = data p in
diff --git a/proofs/proof.mli b/proofs/proof.mli
index 6ef34eed80..7e535a258c 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -47,8 +47,6 @@ type data =
   (** A representation of the shelf  *)
   ; given_up : Evar.t list
   (** A representation of the given up goals  *)
-  ; initial_euctx : UState.t
-  (** The initial universe context (for the statement) *)
   ; name : Names.Id.t
   (** The name of the theorem whose proof is being constructed *)
   ; poly : bool;
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 4490fbdd64..ab8d87c100 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -36,12 +36,13 @@ type 'a proof_entry = {
   proof_entry_inline_code : bool;
 }
 
-type proof_object = {
-  id : Names.Id.t;
-  entries : Evd.side_effects proof_entry list;
-  persistence : Decl_kinds.goal_kind;
-  universes: UState.t;
-}
+type proof_object =
+  { name : Names.Id.t
+  ; entries : Evd.side_effects proof_entry list
+  ; poly : bool
+  ; universes: UState.t
+  ; udecl : UState.universe_decl
+  }
 
 type opacity_flag = Opaque | Transparent
 
@@ -49,15 +50,18 @@ type t =
   { endline_tactic : Genarg.glob_generic_argument option
   ; section_vars : Constr.named_context option
   ; proof : Proof.t
-  ; universe_decl: UState.universe_decl
-  ; strength : Decl_kinds.goal_kind
+  ; udecl: UState.universe_decl
+  (** Initial universe declarations *)
+  ; initial_euctx : UState.t
+  (** The initial universe context (for the statement) *)
   }
 
 (*** Proof Global manipulation ***)
 
 let get_proof ps = ps.proof
 let get_proof_name ps = (Proof.data ps.proof).Proof.name
-let get_persistence ps = ps.strength
+
+let get_initial_euctx ps = ps.initial_euctx
 
 let map_proof f p = { p with proof = f p.proof }
 let map_fold_proof f p = let proof, res = f p.proof in { p with proof }, res
@@ -68,7 +72,8 @@ let map_fold_proof_endline f ps =
     | None -> Proofview.tclUNIT ()
     | Some tac ->
       let open Geninterp in
-      let ist = { lfun = Id.Map.empty; poly = pi2 ps.strength; extra = TacStore.empty } in
+      let {Proof.poly} = Proof.data ps.proof in
+      let ist = { lfun = Id.Map.empty; poly; extra = TacStore.empty } in
       let Genarg.GenArg (Genarg.Glbwit tag, tac) = tac in
       let tac = Geninterp.interp tag ist tac in
       Ftactic.run tac (fun _ -> Proofview.tclUNIT ())
@@ -83,32 +88,33 @@ let compact_the_proof pf = map_proof Proof.compact pf
 let set_endline_tactic tac ps =
   { ps with endline_tactic = Some tac }
 
-(** [start_proof sigma id pl str goals] starts a proof of name
-    [id] with goals [goals] (a list of pairs of environment and
-    conclusion); [str] describes what kind of theorem/definition this
-    is (spiwack: for potential printing, I believe is used only by
-    closing commands and the xml plugin); [terminator] is used at the
-    end of the proof to close the proof. The proof is started in the
-    evar map [sigma] (which can typically contain universe
-    constraints), and with universe bindings pl. *)
-let start_proof sigma name ?(pl=UState.default_univ_decl) kind goals =
-  { proof = Proof.start ~name ~poly:(pi2 kind) sigma goals
+(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of
+   name [name] with goals [goals] (a list of pairs of environment and
+   conclusion). The proof is started in the evar map [sigma] (which
+   can typically contain universe constraints), and with universe
+   bindings [udecl]. *)
+let start_proof ~name ~udecl ~poly sigma goals =
+  let proof = Proof.start ~name ~poly sigma goals in
+  let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
+  { proof
   ; endline_tactic = None
   ; section_vars = None
-  ; universe_decl = pl
-  ; strength = kind
+  ; udecl
+  ; initial_euctx
   }
 
-let start_dependent_proof name ?(pl=UState.default_univ_decl) kind goals =
-  { proof = Proof.dependent_start ~name ~poly:(pi2 kind) goals
+let start_dependent_proof ~name ~udecl ~poly goals =
+  let proof = Proof.dependent_start ~name ~poly goals in
+  let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in
+  { proof
   ; endline_tactic = None
   ; section_vars = None
-  ; universe_decl = pl
-  ; strength = kind
+  ; udecl
+  ; initial_euctx
   }
 
 let get_used_variables pf = pf.section_vars
-let get_universe_decl pf = pf.universe_decl
+let get_universe_decl pf = pf.udecl
 
 let set_used_variables ps l =
   let open Context.Named.Declaration in
@@ -159,8 +165,8 @@ let private_poly_univs =
 
 let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
                 (fpl : closed_proof_output Future.computation) ps =
-  let { section_vars; proof; universe_decl; strength } = ps in
-  let Proof.{ name; poly; entry; initial_euctx } = Proof.data proof in
+  let { section_vars; proof; udecl; initial_euctx } = ps in
+  let Proof.{ name; poly; entry } = Proof.data proof in
   let opaque = match opaque with Opaque -> true | Transparent -> false in
   let constrain_variables ctx =
     UState.constrain_variables (fst (UState.context_set initial_euctx)) ctx
@@ -194,13 +200,13 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
              the body.  So we keep the two sets distinct. *)
           let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
           let ctx_body = UState.restrict ctx used_univs in
-          let univs = UState.check_mono_univ_decl ctx_body universe_decl in
+          let univs = UState.check_mono_univ_decl ctx_body udecl in
           (initunivs, typ), ((body, univs), eff)
         else if poly && opaque && private_poly_univs () then
           let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
           let universes = UState.restrict universes used_univs in
           let typus = UState.restrict universes used_univs_typ in
-          let udecl = UState.check_univ_decl ~poly typus universe_decl in
+          let udecl = UState.check_univ_decl ~poly typus udecl in
           let ubody = Univ.ContextSet.diff
               (UState.context_set universes)
               (UState.context_set typus)
@@ -214,7 +220,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
              TODO: check if restrict is really necessary now. *)
           let used_univs = Univ.LSet.union used_univs_body used_univs_typ in
           let ctx = UState.restrict universes used_univs in
-          let univs = UState.check_univ_decl ~poly ctx universe_decl in
+          let univs = UState.check_univ_decl ~poly ctx udecl in
           (univs, typ), ((body, Univ.ContextSet.empty), eff)
       in 
        fun t p -> Future.split2 (Future.chain p (make_body t))
@@ -236,7 +242,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
               (Vars.universes_of_constr pt)
           in
           let univs = UState.restrict univs used_univs in
-          let univs = UState.check_mono_univ_decl univs universe_decl in
+          let univs = UState.check_mono_univ_decl univs udecl in
           (pt,univs),eff)
   in
   let entry_fn p (_, t) =
@@ -253,8 +259,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
       proof_entry_universes = univs; }
   in
   let entries = Future.map2 entry_fn fpl Proofview.(initial_goals entry) in
-  { id = name; entries = entries; persistence = strength;
-    universes }
+  { name; entries = entries; poly; universes; udecl }
 
 let return_proof ?(allow_partial=false) ps =
  let { proof } = ps in
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 4e1aa64e7b..54d5c2087a 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -17,12 +17,14 @@ type t
 (* Should be moved into a proper view *)
 val get_proof : t -> Proof.t
 val get_proof_name : t -> Names.Id.t
-val get_persistence : t -> Decl_kinds.goal_kind
 val get_used_variables : t -> Constr.named_context option
 
 (** Get the universe declaration associated to the current proof. *)
 val get_universe_decl : t -> UState.universe_decl
 
+(** Get initial universe state *)
+val get_initial_euctx : t -> UState.t
+
 val compact_the_proof : t -> t
 
 (** When a proof is closed, it is reified into a [proof_object], where
@@ -43,37 +45,42 @@ type 'a proof_entry = {
   proof_entry_inline_code : bool;
 }
 
-type proof_object = {
-  id : Names.Id.t;
-  entries : Evd.side_effects proof_entry list;
-  persistence : Decl_kinds.goal_kind;
-  universes: UState.t;
-}
+(** When a proof is closed, it is reified into a [proof_object] *)
+type proof_object =
+  { name : Names.Id.t
+  (** name of the proof *)
+  ; entries : Evd.side_effects proof_entry list
+  (** list of the proof terms (in a form suitable for definitions). *)
+  ; poly : bool
+  (** polymorphic status *)
+  ; universes: UState.t
+  (** universe state *)
+  ; udecl : UState.universe_decl
+  (** universe declaration *)
+  }
 
 type opacity_flag = Opaque | Transparent
 
-(** [start_proof id str pl goals] starts a proof of name
-   [id] with goals [goals] (a list of pairs of environment and
-   conclusion); [str] describes what kind of theorem/definition this
-   is; [terminator] is used at the end of the proof to close the proof
-   (e.g. to declare the built constructions as a coercion or a setoid
-   morphism). The proof is started in the evar map [sigma] (which can
-   typically contain universe constraints), and with universe bindings
-   pl. *)
+(** [start_proof ~name ~udecl ~poly sigma goals] starts a proof of
+   name [name] with goals [goals] (a list of pairs of environment and
+   conclusion); [poly] determines if the proof is universe
+   polymorphic. The proof is started in the evar map [sigma] (which
+   can typically contain universe constraints), and with universe
+   bindings [udecl]. *)
 val start_proof
-  :  Evd.evar_map
-  -> Names.Id.t
-  -> ?pl:UState.universe_decl
-  -> Decl_kinds.goal_kind
+  :  name:Names.Id.t
+  -> udecl:UState.universe_decl
+  -> poly:bool
+  -> Evd.evar_map
   -> (Environ.env * EConstr.types) list
   -> t
 
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
 val start_dependent_proof
-  :  Names.Id.t
-  -> ?pl:UState.universe_decl
-  -> Decl_kinds.goal_kind
+  :  name:Names.Id.t
+  -> udecl:UState.universe_decl
+  -> poly:bool
   -> Proofview.telescope
   -> t
 
diff --git a/stm/stm.ml b/stm/stm.ml
index 89d95d0cc9..28d5447c44 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1537,7 +1537,7 @@ end = struct (* {{{ *)
 
           let st = Vernacstate.freeze_interp_state ~marshallable:false in
           stm_vernac_interp stop
-            ~proof:(pobject, Lemmas.default_info) st
+            ~proof:(pobject, Lemmas.Info.make ()) st
             { verbose = false; indentation = 0; strlen = 0;
               expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in
         ignore(Future.join checked_proof);
@@ -1677,7 +1677,7 @@ end = struct (* {{{ *)
       let pterm, _info =
         PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
 
-      let proof = pterm, Lemmas.default_info in
+      let proof = pterm, Lemmas.Info.make () in
 
       (* We jump at the beginning since the kernel handles side effects by also
        * looking at the ones that happen to be present in the current env *)
@@ -1735,7 +1735,7 @@ end = struct (* {{{ *)
     | `OK (po,_) ->
         let con =
           Nametab.locate_constant
-            (Libnames.qualid_of_ident po.Proof_global.id) in
+            (Libnames.qualid_of_ident po.Proof_global.name) in
         let c = Global.lookup_constant con in
         let o = match c.Declarations.const_body with
           | Declarations.OpaqueDef o -> o
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 4e7f6a0ac6..aaba36287a 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -87,7 +87,7 @@ let classify_vernac e =
         VtProofStep { parallel = `No;
                       proof_block_detection = Some "curly" }
     (* StartProof *)
-    | VernacDefinition ((Decl_kinds.DoDischarge,_),({v=i},_),ProveBody _) ->
+    | VernacDefinition ((DoDischarge,_),({v=i},_),ProveBody _) ->
       VtStartProof(Doesn'tGuaranteeOpacity, idents_of_name i)
 
     | VernacDefinition (_,({v=i},_),ProveBody _) ->
@@ -102,7 +102,7 @@ let classify_vernac e =
     | VernacFixpoint (discharge,l) ->
       let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
        let guarantee =
-         if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
+         if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
          else GuaranteesOpacity
        in
         let ids, open_proof =
@@ -114,7 +114,7 @@ let classify_vernac e =
     | VernacCoFixpoint (discharge,l) ->
       let polymorphic = Attributes.(parse_drop_extra polymorphic atts) in
        let guarantee =
-         if discharge = Decl_kinds.DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
+         if discharge = DoDischarge || polymorphic then Doesn'tGuaranteeOpacity
          else GuaranteesOpacity
        in
         let ids, open_proof =
diff --git a/tactics/abstract.ml b/tactics/abstract.ml
index e4fa5e84b4..465f736032 100644
--- a/tactics/abstract.ml
+++ b/tactics/abstract.ml
@@ -86,10 +86,10 @@ let shrink_entry sign const =
   } in
   (const, args)
 
-let name_op_to_name ~name_op ~name ~goal_kind suffix =
+let name_op_to_name ~name_op ~name suffix =
   match name_op with
-  | Some s -> s, goal_kind
-  | None -> Nameops.add_suffix name suffix, goal_kind
+  | Some s -> s
+  | None -> Nameops.add_suffix name suffix
 
 let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let open Tacticals.New in
@@ -102,10 +102,10 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
      redundancy on constant declaration. This opens up an interesting
      question, how does abstract behave when discharge is local for example?
   *)
-  let goal_kind, suffix = if opaque
-    then (Global ImportDefaultBehavior,poly,Proof Theorem), "_subproof"
-    else (Global ImportDefaultBehavior,poly,DefinitionBody Definition), "_subterm" in
-  let id, goal_kind = name_op_to_name ~name_op ~name ~goal_kind suffix in
+  let suffix = if opaque
+    then "_subproof"
+    else "_subterm" in
+  let name = name_op_to_name ~name_op ~name suffix in
   Proofview.Goal.enter begin fun gl ->
   let env = Proofview.Goal.env gl in
   let sigma = Proofview.Goal.sigma gl in
@@ -121,7 +121,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
         then (s1,push_named_context_val d s2)
         else (Context.Named.add d s1,s2))
       global_sign (Context.Named.empty, Environ.empty_named_context_val) in
-  let id = Namegen.next_global_ident_away id (pf_ids_set_of_hyps gl) in
+  let name = Namegen.next_global_ident_away name (pf_ids_set_of_hyps gl) in
   let concl = match goal_type with
               | None ->  Proofview.Goal.concl gl
               | Some ty -> ty in
@@ -141,7 +141,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
   let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) Tactics.intro) tac) in
   let ectx = Evd.evar_universe_context evd in
   let (const, safe, ectx) =
-    try Pfedit.build_constant_by_tactic ~goal_kind id ectx secsign concl solve_tac
+    try Pfedit.build_constant_by_tactic ~poly ~name ectx secsign concl solve_tac
     with Logic_monad.TacticFailure e as src ->
     (* if the tactic [tac] fails, it reports a [TacticFailure e],
        which is an error irrelevant to the proof system (in fact it
@@ -158,7 +158,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK =
     (* do not compute the implicit arguments, it may be costly *)
     let () = Impargs.make_implicit_args false in
     (* ppedrot: seems legit to have abstracted subproofs as local*)
-    Declare.declare_private_constant ~internal:Declare.InternalTacticRequest ~local:ImportNeedQualified id decl
+    Declare.declare_private_constant ~internal:Declare.InternalTacticRequest ~local:Declare.ImportNeedQualified name decl
   in
   let cst, eff = Impargs.with_implicit_protection cst () in
   let inst = match const.Proof_global.proof_entry_universes with
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 339d4de2a0..499e7a63d7 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -69,7 +69,7 @@ let auto_unif_flags =
 
 (* Try unification with the precompiled clause, then use registered Apply *)
 
-let connect_hint_clenv poly (c, _, ctx) clenv gl =
+let connect_hint_clenv ~poly (c, _, ctx) clenv gl =
   (* [clenv] has been generated by a hint-making function, so the only relevant
      data in its evarmap is the set of metas. The [evar_reset_evd] function
      below just replaces the metas of sigma by those coming from the clenv. *)
@@ -95,22 +95,22 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
       { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
   in clenv, c
 
-let unify_resolve poly flags ((c : raw_hint), clenv) =
+let unify_resolve ~poly flags ((c : raw_hint), clenv) =
   Proofview.Goal.enter begin fun gl ->
-  let clenv, c = connect_hint_clenv poly c clenv gl in
+  let clenv, c = connect_hint_clenv ~poly c clenv gl in
   let clenv = clenv_unique_resolver ~flags clenv gl in
   Clenvtac.clenv_refine clenv
   end
 
-let unify_resolve_nodelta poly h = unify_resolve poly auto_unif_flags h
+let unify_resolve_nodelta poly h = unify_resolve ~poly auto_unif_flags h
 
-let unify_resolve_gen poly = function
+let unify_resolve_gen ~poly = function
   | None -> unify_resolve_nodelta poly
-  | Some flags -> unify_resolve poly flags
+  | Some flags -> unify_resolve ~poly flags
 
 let exact poly (c,clenv) =
   Proofview.Goal.enter begin fun gl ->
-    let clenv', c = connect_hint_clenv poly c clenv gl in
+    let clenv', c = connect_hint_clenv ~poly c clenv gl in
     Tacticals.New.tclTHEN
     (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
     (exact_check c)
@@ -378,12 +378,12 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
 
 and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) =
   let tactic = function
-    | Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl)
+    | Res_pf (c,cl) -> unify_resolve_gen ~poly flags (c,cl)
     | ERes_pf _ -> Proofview.Goal.enter (fun gl -> Tacticals.New.tclZEROMSG (str "eres_pf"))
     | Give_exact (c, cl)  -> exact poly (c, cl)
     | Res_pf_THEN_trivial_fail (c,cl) ->
       Tacticals.New.tclTHEN
-        (unify_resolve_gen poly flags (c,cl))
+        (unify_resolve_gen ~poly flags (c,cl))
 	(* With "(debug) trivial", we shouldn't end here, and
 	   with "debug auto" we don't display the details of inner trivial *)
         (trivial_fail_db (no_dbg dbg) (not (Option.is_empty flags)) db_list local_db)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index a834b4b12d..5ae63be539 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -14,7 +14,6 @@ open Names
 open EConstr
 open Clenv
 open Pattern
-open Decl_kinds
 open Hints
 open Tactypes
 
@@ -24,11 +23,11 @@ val default_search_depth : int ref
 
 val auto_flags_of_state : TransparentState.t -> Unification.unify_flags
 
-val connect_hint_clenv : polymorphic -> raw_hint -> clausenv ->
-  Proofview.Goal.t -> clausenv * constr
+val connect_hint_clenv
+  : poly:bool -> raw_hint -> clausenv -> Proofview.Goal.t -> clausenv * constr
 
 (** Try unification with the precompiled clause, then use registered Apply *)
-val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic
+val unify_resolve : poly:bool -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic
 
 (** [ConclPattern concl pat tacast]:
    if the term concl matches the pattern pat, (in sense of
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index b0fb47726a..303ddacb67 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -204,11 +204,11 @@ let clenv_unique_resolver_tac with_evars ~flags clenv' =
   end
 
 let unify_e_resolve poly flags = begin fun gls (c,_,clenv) ->
-  let clenv', c = connect_hint_clenv poly c clenv gls in
+  let clenv', c = connect_hint_clenv ~poly c clenv gls in
   clenv_unique_resolver_tac true ~flags clenv' end
 
 let unify_resolve poly flags = begin fun gls (c,_,clenv) ->
-  let clenv', _ = connect_hint_clenv poly c clenv gls in
+  let clenv', _ = connect_hint_clenv ~poly c clenv gls in
   clenv_unique_resolver_tac false ~flags clenv'
   end
 
@@ -536,7 +536,7 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
             (List.map_append
              (fun (path,info,c) ->
               make_resolves env sigma ~name:(PathHints path)
-                  (true,false,not !Flags.quiet) info false
+                  (true,false,not !Flags.quiet) info ~poly:false
                  (IsConstr (EConstr.of_constr c,Univ.ContextSet.empty)))
                hints)
         else []
@@ -544,8 +544,8 @@ let make_resolve_hyp env sigma st flags only_classes pri decl =
         (hints @ List.map_filter
          (fun f -> try Some (f (c, cty, Univ.ContextSet.empty))
            with Failure _ | UserError _ -> None)
-         [make_exact_entry ~name env sigma pri false;
-          make_apply_entry ~name env sigma flags pri false])
+         [make_exact_entry ~name env sigma pri ~poly:false;
+          make_apply_entry ~name env sigma flags pri ~poly:false])
     else []
 
 let make_hints g (modes,st) only_classes sign =
diff --git a/tactics/declare.ml b/tactics/declare.ml
index ca5d265733..4a4e2cf60a 100644
--- a/tactics/declare.ml
+++ b/tactics/declare.ml
@@ -33,6 +33,8 @@ type internal_flag =
   | InternalTacticRequest  (* kernel action, no message is displayed *)
   | UserIndividualRequest   (* user action, a message is displayed *)
 
+type import_status = ImportDefaultBehavior | ImportNeedQualified
+
 (** Declaration of constants and parameters *)
 
 type constant_obj = {
@@ -96,7 +98,7 @@ let cache_constant ((sp,kn), obj) =
   assert (Constant.equal kn' (Constant.make1 kn));
   Nametab.push (Nametab.Until 1) sp (ConstRef (Constant.make1 kn));
   let cst = Global.lookup_constant kn' in
-  add_section_constant (Declareops.constant_is_polymorphic cst) kn' cst.const_hyps;
+  add_section_constant ~poly:(Declareops.constant_is_polymorphic cst) kn' cst.const_hyps;
   add_constant_kind (Constant.make1 kn) obj.cst_kind
 
 let discharge_constant ((sp, kn), obj) =
@@ -262,23 +264,23 @@ let declare_definition ?(internal=UserIndividualRequest)
 (** Declaration of section variables and local definitions *)
 type section_variable_entry =
   | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
-  | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
+  | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool }
 
 type variable_declaration = DirPath.t * section_variable_entry * logical_kind
 
 let cache_variable ((sp,_),o) =
   match o with
   | Inl ctx -> Global.push_context_set false ctx
-  | Inr (id,(p,d,mk)) ->
+  | Inr (id,(path,d,kind)) ->
   (* Constr raisonne sur les noms courts *)
   if variable_exists id then
     alreadydeclared (Id.print id ++ str " already exists");
 
-  let impl,opaq,poly,ctx = match d with (* Fails if not well-typed *)
-    | SectionLocalAssum ((ty,ctx),poly,impl) ->
-      let () = Global.push_named_assum ((id,ty,poly),ctx) in
+  let impl,opaque,poly,univs = match d with (* Fails if not well-typed *)
+    | SectionLocalAssum {typ;univs;poly;impl} ->
+      let () = Global.push_named_assum ((id,typ,poly),univs) in
       let impl = if impl then Implicit else Explicit in
-        impl, true, poly, ctx
+        impl, true, poly, univs
     | SectionLocalDef (de) ->
       (* The body should already have been forced upstream because it is a
          section-local definition, but it's not enforced by typing *)
@@ -305,8 +307,8 @@ let cache_variable ((sp,_),o) =
       Explicit, de.proof_entry_opaque,
       poly, univs in
   Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
-  add_section_variable id impl poly ctx;
-  add_variable_data id (p,opaq,ctx,poly,mk)
+  add_section_variable ~name:id ~kind:impl ~poly univs;
+  add_variable_data id {path;opaque;univs;poly;kind}
 
 let discharge_variable (_,o) = match o with
   | Inr (id,_) ->
@@ -374,7 +376,7 @@ let cache_inductive ((sp,kn),mie) =
   let kn' = Global.add_mind id mie in
   assert (MutInd.equal kn' (MutInd.make1 kn));
   let mind = Global.lookup_mind kn' in
-  add_section_kn (Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
+  add_section_kn ~poly:(Declareops.inductive_is_polymorphic mind) kn' mind.mind_hyps;
   List.iter (fun (sp, ref) -> Nametab.push (Nametab.Until 1) sp ref) names
 
 let discharge_inductive ((sp,kn),mie) =
@@ -525,7 +527,7 @@ let input_universe_context : Univ.ContextSet.t -> Libobject.obj =
     ~cache:(fun (na, uctx) -> Global.push_context_set false uctx)
     ~discharge:(fun (_, x) -> Some x)
 
-let declare_universe_context poly ctx =
+let declare_universe_context ~poly ctx =
   if poly then
     (Global.push_context_set true ctx; Lib.add_section_context ctx)
   else
@@ -605,7 +607,7 @@ let declare_univ_binders gr pl =
     in
     Lib.add_anonymous_leaf (input_univ_names (QualifiedUniv l, univs))
 
-let do_universe poly l =
+let do_universe ~poly l =
   let in_section = Lib.sections_are_opened () in
   let () =
     if poly && not in_section then
@@ -616,11 +618,11 @@ let do_universe poly l =
   let ctx = List.fold_left (fun ctx (_,qid) -> Univ.LSet.add (Univ.Level.make qid) ctx)
       Univ.LSet.empty l, Univ.Constraint.empty
   in
-  let () = declare_universe_context poly ctx in
+  let () = declare_universe_context ~poly ctx in
   let src = if poly then BoundUniv else UnqualifiedUniv in
   Lib.add_anonymous_leaf (input_univ_names (src, l))
 
-let do_constraint poly l =
+let do_constraint ~poly l =
   let open Univ in
   let u_of_id x =
     let level = Pretyping.interp_known_glob_level (Evd.from_env (Global.env ())) x in
@@ -647,4 +649,4 @@ let do_constraint poly l =
     Constraint.empty l
   in
   let uctx = ContextSet.add_constraints constraints ContextSet.empty in
-  declare_universe_context poly uctx
+  declare_universe_context ~poly uctx
diff --git a/tactics/declare.mli b/tactics/declare.mli
index 0a2332748c..d87c096119 100644
--- a/tactics/declare.mli
+++ b/tactics/declare.mli
@@ -24,7 +24,7 @@ open Decl_kinds
 
 type section_variable_entry =
   | SectionLocalDef of Evd.side_effects Proof_global.proof_entry
-  | SectionLocalAssum of types Univ.in_universe_context_set * polymorphic * bool (** Implicit status *)
+  | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool }
 
 type 'a constant_entry =
   | DefinitionEntry of 'a Proof_global.proof_entry
@@ -51,6 +51,8 @@ val definition_entry : ?fix_exn:Future.fix_exn ->
   ?univs:Entries.universes_entry ->
   ?eff:Evd.side_effects -> constr -> Evd.side_effects Proof_global.proof_entry
 
+type import_status = ImportDefaultBehavior | ImportNeedQualified
+
 (** [declare_constant id cd] declares a global declaration
    (constant/parameter) with name [id] in the current section; it returns
    the full path of the declaration
@@ -92,7 +94,7 @@ val exists_name : Id.t -> bool
 (** Global universe contexts, names and constraints *)
 val declare_univ_binders : GlobRef.t -> UnivNames.universe_binders -> unit
 
-val declare_universe_context : polymorphic -> Univ.ContextSet.t -> unit
+val declare_universe_context : poly:bool -> Univ.ContextSet.t -> unit
 
-val do_universe : polymorphic -> lident list -> unit
-val do_constraint : polymorphic -> Glob_term.glob_constraint list -> unit
+val do_universe : poly:bool -> lident list -> unit
+val do_constraint : poly:bool -> Glob_term.glob_constraint list -> unit
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index ac6253cf40..cc3e78f3b8 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -113,7 +113,7 @@ let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
 
 let unify_e_resolve poly flags (c,clenv) =
   Proofview.Goal.enter begin fun gl ->
-      let clenv', c = connect_hint_clenv poly c clenv gl in
+      let clenv', c = connect_hint_clenv ~poly c clenv gl in
       let clenv' = clenv_unique_resolver ~flags clenv' gl in
       Proofview.tclTHEN
         (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
@@ -131,7 +131,7 @@ let hintmap_of sigma secvars hdc concl =
 
 let e_exact poly flags (c,clenv) =
   Proofview.Goal.enter begin fun gl ->
-    let clenv', c = connect_hint_clenv poly c clenv gl in
+    let clenv', c = connect_hint_clenv ~poly c clenv gl in
     Tacticals.New.tclTHEN
     (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
     (e_give_exact c)
@@ -168,7 +168,7 @@ and e_my_find_search env sigma db_list local_db secvars hdc concl =
       in
       (b,
         let tac = function
-        | Res_pf (term,cl) -> unify_resolve poly st (term,cl)
+        | Res_pf (term,cl) -> unify_resolve ~poly st (term,cl)
         | ERes_pf (term,cl) -> unify_e_resolve poly st (term,cl)
         | Give_exact (c,cl) -> e_exact poly st (c,cl)
         | Res_pf_THEN_trivial_fail (term,cl) ->
diff --git a/tactics/hints.ml b/tactics/hints.ml
index e824c4bd64..014e54158d 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -27,7 +27,6 @@ open Smartlocate
 open Termops
 open Inductiveops
 open Typing
-open Decl_kinds
 open Typeclasses
 open Pattern
 open Patternops
@@ -142,15 +141,22 @@ type raw_hint = constr * types * Univ.ContextSet.t
 
 type hint = (raw_hint * clausenv) hint_ast with_uid
 
-type 'a with_metadata = {
-  pri     : int;            (* A number lower is higher priority *)
-  poly    : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
-  pat     : constr_pattern option; (* A pattern for the concl of the Goal *)
-  name    : hints_path_atom; (* A potential name to refer to the hint *)
-  db : string option; (** The database from which the hint comes *)
-  secvars : Id.Pred.t; (* The set of section variables the hint depends on *)
-  code    : 'a;     (* the tactic to apply when the concl matches pat *)
-}
+type 'a with_metadata =
+  { pri     : int
+  (** A number lower is higher priority *)
+  ; poly    : bool
+  (** Is the hint polymorpic and hence should be refreshed at each application *)
+  ; pat     : constr_pattern option
+  (** A pattern for the concl of the Goal *)
+  ; name    : hints_path_atom
+  (** A potential name to refer to the hint *)
+  ; db : string option
+  (** The database from which the hint comes *)
+  ; secvars : Id.Pred.t
+  (** The set of section variables the hint depends on *)
+  ; code    : 'a
+  (** the tactic to apply when the concl matches pat *)
+  }
 
 type full_hint = hint with_metadata
 
@@ -792,7 +798,7 @@ let secvars_of_constr env sigma c =
 let secvars_of_global env gr =
   secvars_of_idset (vars_of_global env gr)
 
-let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) =
+let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) =
   let secvars = secvars_of_constr env sigma c in
   let cty = strip_outer_cast sigma cty in
     match EConstr.kind sigma cty with
@@ -813,7 +819,7 @@ let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) =
 	   db = None; secvars;
 	   code = with_uid (Give_exact (c, cty, ctx)); })
 
-let make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c, cty, ctx) =
+let make_apply_entry env sigma (eapply,hnf,verbose) info ~poly ?(name=PathAny) (c, cty, ctx) =
   let cty = if hnf then hnf_constr env sigma cty else cty in
   match EConstr.kind sigma cty with
   | Prod _ ->
@@ -887,18 +893,18 @@ let fresh_global_or_constr env sigma poly cr =
     else begin
       if isgr then
         warn_polymorphic_hint (pr_hint_term env sigma ctx cr);
-      Declare.declare_universe_context false ctx;
+      Declare.declare_universe_context ~poly:false ctx;
       (c, Univ.ContextSet.empty)
     end
 
-let make_resolves env sigma flags info poly ?name cr =
+let make_resolves env sigma flags info ~poly ?name cr =
   let c, ctx = fresh_global_or_constr env sigma poly cr in
   let cty = Retyping.get_type_of env sigma c in
   let try_apply f =
     try Some (f (c, cty, ctx)) with Failure _ -> None in
   let ents = List.map_filter try_apply
-			     [make_exact_entry env sigma info poly ?name;
-			      make_apply_entry env sigma flags info poly ?name]
+                             [make_exact_entry env sigma info ~poly ?name;
+                              make_apply_entry env sigma flags info ~poly ?name]
   in
   if List.is_empty ents then
     user_err ~hdr:"Hint"
@@ -912,7 +918,7 @@ let make_resolve_hyp env sigma decl =
   let hname = NamedDecl.get_id decl in
   let c = mkVar hname in
   try
-    [make_apply_entry env sigma (true, true, false) empty_hint_info false
+    [make_apply_entry env sigma (true, true, false) empty_hint_info ~poly:false
        ~name:(PathHints [VarRef hname])
        (c, NamedDecl.get_type decl, Univ.ContextSet.empty)]
   with
@@ -1178,7 +1184,7 @@ let add_resolves env sigma clist local dbnames =
       let r =
         List.flatten (List.map (fun (pri, poly, hnf, path, gr) ->
           make_resolves env sigma (true,hnf,not !Flags.quiet)
-            pri poly ~name:path gr) clist)
+            pri ~poly ~name:path gr) clist)
       in
       let hint = make_hint ~local dbname (AddHints r) in
       Lib.add_anonymous_leaf (inAutoHint hint))
@@ -1238,8 +1244,8 @@ type hnf = bool
 type nonrec hint_info = hint_info
 
 type hints_entry =
-  | HintsResolveEntry of (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list
-  | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list
+  | HintsResolveEntry of (hint_info * bool * hnf * hints_path_atom * hint_term) list
+  | HintsImmediateEntry of (hints_path_atom * bool * hint_term) list
   | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool
@@ -1286,7 +1292,7 @@ let prepare_hint check (poly,local) env init (sigma,c) =
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
     if poly then IsConstr (c', diff)
     else if local then IsConstr (c', diff)
-    else (Declare.declare_universe_context false diff;
+    else (Declare.declare_universe_context ~poly:false diff;
 	  IsConstr (c', Univ.ContextSet.empty))
 
 let project_hint ~poly pri l2r r =
@@ -1318,7 +1324,7 @@ let project_hint ~poly pri l2r r =
   let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in
     (info,false,true,PathAny, IsGlobRef (Globnames.ConstRef c))
 
-let interp_hints poly =
+let interp_hints ~poly =
   fun h ->
   let env = Global.env () in
   let sigma = Evd.from_env env in
@@ -1417,7 +1423,7 @@ let expand_constructor_hints env sigma lems =
 let constructor_hints env sigma eapply lems =
   let lems = expand_constructor_hints env sigma lems in
   List.map_append (fun (poly, lem) ->
-      make_resolves env sigma (eapply,true,false) empty_hint_info poly lem) lems
+      make_resolves env sigma (eapply,true,false) empty_hint_info ~poly lem) lems
 
 let make_local_hint_db env sigma ts eapply lems =
   let map c = c env sigma in
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 839ef31189..4c82a068b1 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -12,7 +12,6 @@ open Util
 open Names
 open EConstr
 open Environ
-open Decl_kinds
 open Evd
 open Tactypes
 open Clenv
@@ -54,15 +53,22 @@ type 'a hints_path_atom_gen =
 type hints_path_atom = GlobRef.t hints_path_atom_gen
 type hint_db_name = string
 
-type 'a with_metadata = private {
-  pri   : int;            (** A number between 0 and 4, 4 = lower priority *)
-  poly  : polymorphic;    (** Is the hint polymorpic and hence should be refreshed at each application *)
-  pat   : constr_pattern option; (** A pattern for the concl of the Goal *)
-  name  : hints_path_atom; (** A potential name to refer to the hint *) 
-  db    : hint_db_name option;
-  secvars : Id.Pred.t; (** The section variables this hint depends on, as a predicate *)
-  code    : 'a; (** the tactic to apply when the concl matches pat *)
-}
+type 'a with_metadata = private
+  { pri     : int
+  (** A number lower is higher priority *)
+  ; poly    : bool
+  (** Is the hint polymorpic and hence should be refreshed at each application *)
+  ; pat     : constr_pattern option
+  (** A pattern for the concl of the Goal *)
+  ; name    : hints_path_atom
+  (** A potential name to refer to the hint *)
+  ; db : string option
+  (** The database from which the hint comes *)
+  ; secvars : Id.Pred.t
+  (** The set of section variables the hint depends on *)
+  ; code    : 'a
+  (** the tactic to apply when the concl matches pat *)
+  }
 
 type full_hint = hint with_metadata
 
@@ -176,9 +182,8 @@ type hint_term =
   | IsConstr of constr * Univ.ContextSet.t
 
 type hints_entry =
-  | HintsResolveEntry of
-    (hint_info * polymorphic * hnf * hints_path_atom * hint_term) list
-  | HintsImmediateEntry of (hints_path_atom * polymorphic * hint_term) list
+  | HintsResolveEntry of (hint_info * bool * hnf * hints_path_atom * hint_term) list
+  | HintsImmediateEntry of (hints_path_atom * bool * hint_term) list
   | HintsCutEntry of hints_path
   | HintsUnfoldEntry of evaluable_global_reference list
   | HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool
@@ -202,7 +207,7 @@ val current_db_names : unit -> String.Set.t
 
 val current_pure_db : unit -> hint_db list
 
-val interp_hints : polymorphic -> hints_expr -> hints_entry
+val interp_hints : poly:bool -> hints_expr -> hints_entry
 
 val add_hints : local:bool -> hint_db_name list -> hints_entry -> unit
 
@@ -219,7 +224,7 @@ val prepare_hint : bool (* Check no remaining evars *) ->
    [hint_pattern] is the hint's desired pattern, it is inferred if not specified
 *)
 
-val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hints_path_atom ->
+val make_exact_entry : env -> evar_map -> hint_info -> poly:bool -> ?name:hints_path_atom ->
   (constr * types * Univ.ContextSet.t) -> hint_entry
 
 (** [make_apply_entry (eapply,hnf,verbose) info (c,cty,ctx))].
@@ -237,7 +242,7 @@ val make_exact_entry : env -> evar_map -> hint_info -> polymorphic -> ?name:hint
 *)
 
 val make_apply_entry :
-  env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom ->
+  env -> evar_map -> bool * bool * bool -> hint_info -> poly:bool -> ?name:hints_path_atom ->
   (constr * types * Univ.ContextSet.t) -> hint_entry
 
 (** A constr which is Hint'ed will be:
@@ -248,7 +253,7 @@ val make_apply_entry :
          has missing arguments. *)
 
 val make_resolves :
-  env -> evar_map -> bool * bool * bool -> hint_info -> polymorphic -> ?name:hints_path_atom ->
+  env -> evar_map -> bool * bool * bool -> hint_info -> poly:bool -> ?name:hints_path_atom ->
   hint_term -> hint_entry list
 
 (** [make_resolve_hyp hname htyp].
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 ->