Merge PR #11818: [proof] Further consolidation of the regular declaration path

Ack-by: Matafou
Reviewed-by: SkySkimmer

24 files changed, 787 insertions, 655 deletions

diff --git a/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh
new file mode 100644
index 0000000000..e3a8eb07f3
--- /dev/null
+++ b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "11818" ] || [ "$CI_BRANCH" = "proof+remove_special_case_first_declaration_in_mutual" ]; then
+
+    metacoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+    metacoq_CI_GITURL=https://github.com/ejgallego/metacoq
+
+    elpi_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+    paramcoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+    equations_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
diff --git a/doc/plugin_tutorial/tuto1/src/simple_declare.ml b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
index 2fdca15552..8c4dc0e8a6 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_declare.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_declare.ml
@@ -1,10 +1,6 @@
 let edeclare ?hook ~name ~poly ~scope ~kind ~opaque ~udecl ~impargs sigma body tyopt  =
-  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 ubind = Evd.universe_binders sigma in
-  let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
-  DeclareDef.declare_definition ~name ~scope ~kind ~ubind ce ~impargs ?hook_data
+  DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook
+    ~opaque ~poly ~udecl ~types:tyopt ~body sigma
 
 let declare_definition ~poly name sigma body =
   let udecl = UState.default_univ_decl in
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml
index 446026c4c8..45c46c56f4 100644
--- a/plugins/funind/gen_principle.ml
+++ b/plugins/funind/gen_principle.ml
@@ -199,7 +199,7 @@ let build_functional_principle ?(opaque=Proof_global.Transparent) (evd:Evd.evar_
   (*    end; *)
 
   let open Proof_global in
-  let { name; entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in
+  let { entries } = Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x)) lemma in
   match entries with
   | [entry] ->
     entry, hook
@@ -290,14 +290,12 @@ 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
-  let hook_data = hook, uctx, [] in
-  let _ : Names.GlobRef.t = DeclareDef.declare_definition
-      ~name:new_princ_name ~hook_data
+  let _ : Names.GlobRef.t = DeclareDef.declare_entry
+      ~name:new_princ_name ~hook
       ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
       ~kind:Decls.(IsProof Theorem)
-      ~ubind:UnivNames.empty_binders
       ~impargs:[]
-      entry in
+      ~uctx entry in
   ()
   with e when CErrors.noncritical e ->
     raise (Defining_principle e)
@@ -375,7 +373,6 @@ let register_struct is_rec fixpoint_exprl =
       | None ->
         CErrors.user_err ~hdr:"Function" Pp.(str "Body of Function must be given") in
     ComDefinition.do_definition
-      ~program_mode:false
       ~name:fname.CAst.v
       ~poly:false
       ~scope:(DeclareDef.Global Declare.ImportDefaultBehavior)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ded159e484..52122c09df 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -231,7 +231,7 @@ let frozen_and_pending_holes (sigma, sigma') =
     end in
     FrozenProgress data
 
-let apply_typeclasses ~program_mode env sigma frozen fail_evar =
+let apply_typeclasses ~program_mode ~fail_evar env sigma frozen =
   let filter_frozen = match frozen with
     | FrozenId map -> fun evk -> Evar.Map.mem evk map
     | FrozenProgress (lazy (frozen, _)) -> fun evk -> Evar.Set.mem evk frozen
@@ -270,7 +270,7 @@ let apply_heuristics env sigma fail_evar =
 
 let check_typeclasses_instances_are_solved ~program_mode env current_sigma frozen =
   (* Naive way, call resolution again with failure flag *)
-  apply_typeclasses ~program_mode env current_sigma frozen true
+  apply_typeclasses ~program_mode ~fail_evar:true env current_sigma frozen
 
 let check_extra_evars_are_solved env current_sigma frozen = match frozen with
 | FrozenId _ -> ()
@@ -313,7 +313,7 @@ let solve_remaining_evars ?hook flags env ?initial sigma =
   let frozen = frozen_and_pending_holes (initial, sigma) in
   let sigma =
     if flags.use_typeclasses
-    then apply_typeclasses ~program_mode env sigma frozen false
+    then apply_typeclasses ~fail_evar:false ~program_mode env sigma frozen
     else sigma
   in
   let sigma = match hook with
diff --git a/tactics/proof_global.ml b/tactics/proof_global.ml
index 623e6b8a42..620afbaf23 100644
--- a/tactics/proof_global.ml
+++ b/tactics/proof_global.ml
@@ -18,9 +18,9 @@ module NamedDecl = Context.Named.Declaration
 
 type proof_object =
   { name : Names.Id.t
+  (* [name] only used in the STM *)
   ; entries : Evd.side_effects Declare.proof_entry list
   ; uctx: UState.t
-  ; udecl : UState.universe_decl
   }
 
 type opacity_flag = Opaque | Transparent
@@ -231,7 +231,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ?feedback_id ~now
     Declare.delayed_definition_entry ~opaque ?feedback_id ?section_vars ~univs ~types:typ body
   in
   let entries = Future.map2 entry_fn fpl (Proofview.initial_goals entry) in
-  { name; entries; uctx; udecl }
+  { name; entries; uctx }
 
 let return_proof ?(allow_partial=false) ps =
  let { proof } = ps in
diff --git a/tactics/proof_global.mli b/tactics/proof_global.mli
index e1c75c0649..d820fc8b40 100644
--- a/tactics/proof_global.mli
+++ b/tactics/proof_global.mli
@@ -33,8 +33,6 @@ type proof_object =
   (** list of the proof terms (in a form suitable for definitions). *)
   ; uctx: UState.t
   (** universe state *)
-  ; udecl : UState.universe_decl
-  (** universe declaration *)
   }
 
 type opacity_flag = Opaque | Transparent
diff --git a/vernac/classes.ml b/vernac/classes.ml
index dafd1cc5e4..6e929de581 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -304,22 +304,19 @@ let id_of_class cl =
           mip.(0).Declarations.mind_typename
     | _ -> assert false
 
-let instance_hook info global imps ?hook cst =
-  Impargs.maybe_declare_manual_implicits false cst imps;
+let instance_hook info global ?hook cst =
   let info = intern_info info in
   let env = Global.env () in
   let sigma = Evd.from_env env in
   declare_instance env sigma (Some info) (not global) cst;
   (match hook with Some h -> h cst | None -> ())
 
-let declare_instance_constant info global imps ?hook name udecl poly sigma term termtype =
+let declare_instance_constant info global impargs ?hook name udecl poly sigma term termtype =
   let kind = Decls.(IsDefinition Instance) in
-  let sigma, entry = DeclareDef.prepare_definition
-      ~allow_evars:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in
-  let kn = Declare.declare_constant ~name ~kind (Declare.DefinitionEntry entry) in
-  Declare.definition_message name;
-  DeclareUniv.declare_univ_binders (GlobRef.ConstRef kn) (Evd.universe_binders sigma);
-  instance_hook info global imps ?hook (GlobRef.ConstRef kn)
+  let scope = DeclareDef.Global Declare.ImportDefaultBehavior in
+  let kn = DeclareDef.declare_definition ~name ~kind ~scope ~impargs
+      ~opaque:false ~poly sigma ~udecl ~types:(Some termtype) ~body:term in
+  instance_hook info global ?hook kn
 
 let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst name =
   let subst = List.fold_left2
@@ -328,30 +325,31 @@ let do_declare_instance sigma ~global ~poly k u ctx ctx' pri udecl impargs subst
   in
   let (_, ty_constr) = instance_constructor (k,u) subst in
   let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
-  let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma ~udecl ~types:termtype in
+  let sigma, entry = DeclareDef.prepare_parameter ~poly sigma ~udecl ~types:termtype in
   let cst = Declare.declare_constant ~name
       ~kind:Decls.(IsAssumption Logical) (Declare.ParameterEntry entry) in
   DeclareUniv.declare_univ_binders (GlobRef.ConstRef cst) (Evd.universe_binders sigma);
-  instance_hook pri global impargs (GlobRef.ConstRef cst)
+  let cst = (GlobRef.ConstRef cst) in
+  Impargs.maybe_declare_manual_implicits false cst impargs;
+  instance_hook pri global cst
 
-let declare_instance_program env sigma ~global ~poly name pri imps udecl term termtype =
+let declare_instance_program env sigma ~global ~poly name pri impargs udecl term termtype =
   let hook { DeclareDef.Hook.S.scope; dref; _ } =
     let cst = match dref with GlobRef.ConstRef kn -> kn | _ -> assert false in
-    Impargs.declare_manual_implicits false dref imps;
     let pri = intern_info pri in
     let env = Global.env () in
     let sigma = Evd.from_env env in
     declare_instance env sigma (Some pri) (not global) (GlobRef.ConstRef cst)
   in
-  let obls, _, term, typ = Obligations.eterm_obligations env name sigma 0 term termtype in
+  let obls, _, term, typ = RetrieveObl.retrieve_obligations env name sigma 0 term termtype in
   let hook = DeclareDef.Hook.make hook in
   let uctx = Evd.evar_universe_context sigma in
   let scope, kind = DeclareDef.Global Declare.ImportDefaultBehavior, Decls.Instance in
   let _ : DeclareObl.progress =
-    Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook typ ~uctx obls
+    Obligations.add_definition ~name ~term ~udecl ~scope ~poly ~kind ~hook ~impargs ~uctx typ obls
   in ()
 
-let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids term termtype =
+let declare_instance_open sigma ?hook ~tac ~global ~poly id pri impargs 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
@@ -359,12 +357,12 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps udecl ids t
   let gls = List.rev (Evd.future_goals sigma) in
   let sigma = Evd.reset_future_goals sigma in
   let kind = Decls.(IsDefinition Instance) in
-  let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global imps ?hook dref)) in
+  let hook = DeclareDef.Hook.(make (fun { S.dref ; _ } -> instance_hook pri global ?hook dref)) in
   let info = Lemmas.Info.make ~hook ~kind () in
   (* XXX: We need to normalize the type, otherwise Admitted / Qed will fails!
      This is due to a bug in proof_global :( *)
   let termtype = Evarutil.nf_evar sigma termtype in
-  let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info sigma termtype in
+  let lemma = Lemmas.start_lemma ~name:id ~poly ~udecl ~info ~impargs sigma termtype in
   (* spiwack: I don't know what to do with the status here. *)
   let lemma =
     match term with
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index dc9c8e2d3c..47ae03e0a3 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -203,8 +203,12 @@ let context_insection sigma ~poly ctx =
           else Monomorphic_entry Univ.ContextSet.empty
         in
         let entry = Declare.definition_entry ~univs ~types:t b in
-        let _ : GlobRef.t = DeclareDef.declare_definition ~name ~scope:DeclareDef.Discharge
-            ~kind:Decls.(IsDefinition Definition) ~ubind:UnivNames.empty_binders ~impargs:[] entry
+        (* XXX Fixme: Use DeclareDef.prepare_definition *)
+        let uctx = Evd.evar_universe_context sigma in
+        let kind = Decls.(IsDefinition Definition) in
+        let _ : GlobRef.t =
+          DeclareDef.declare_entry ~name ~scope:DeclareDef.Discharge
+            ~kind ~impargs:[] ~uctx entry
         in
         ()
     in
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index d50edbad4d..8a91e9e63f 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -12,7 +12,6 @@ open Pp
 open Util
 open Redexpr
 open Constrintern
-open Pretyping
 
 (* Commands of the interface: Constant definitions *)
 
@@ -108,41 +107,26 @@ let interp_definition ~program_mode pl bl ~poly red_option c ctypopt =
   (* Declare the definition *)
   let c = EConstr.it_mkLambda_or_LetIn c ctx in
   let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in
+  (c, tyopt), evd, udecl, imps
 
-  let evd, ce = DeclareDef.prepare_definition ~allow_evars:program_mode
-      ~opaque:false ~poly evd ~udecl ~types:tyopt ~body:c in
-
-  (ce, evd, udecl, imps)
-
-let check_definition ~program_mode (ce, evd, _, imps) =
-  let env = Global.env () in
-  check_evars_are_solved ~program_mode env evd;
-  ce
+let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
+  let program_mode = false in
+  let (body, types), evd, udecl, impargs =
+    interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
+  in
+  let kind = Decls.IsDefinition kind in
+  let _ : Names.GlobRef.t =
+    DeclareDef.declare_definition ~name ~scope ~kind ?hook ~impargs
+      ~opaque:false ~poly evd ~udecl ~types ~body
+  in ()
 
-let do_definition ~program_mode ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
-  let (ce, evd, udecl, impargs as def) =
+let do_definition_program ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt =
+  let program_mode = true in
+  let (body, types), evd, udecl, impargs =
     interp_definition ~program_mode udecl bl ~poly red_option c ctypopt
   in
-  if program_mode then
-    let env = Global.env () in
-    let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in
-    assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private);
-    assert(Univ.ContextSet.is_empty ctx);
-    Obligations.check_evars env evd;
-    let c = EConstr.of_constr c in
-    let typ = match ce.Declare.proof_entry_type with
-      | Some t -> EConstr.of_constr t
-      | None -> Retyping.get_type_of env evd c
-    in
-    let obls, _, c, cty =
-      Obligations.eterm_obligations env name evd 0 c typ
-    in
-    let uctx = Evd.evar_universe_context evd in
-    ignore(Obligations.add_definition
-             ~name ~term:c cty ~uctx ~udecl ~impargs ~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
-    let kind = Decls.IsDefinition kind in
-    ignore(DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind:(Evd.universe_binders evd) ce ~impargs)
+  let term, ty, uctx, obls = DeclareDef.prepare_obligation ~name ~poly ~body ~types ~udecl evd in
+  let _ : DeclareObl.progress =
+    Obligations.add_definition
+      ~name ~term ty ~uctx ~udecl ~impargs ~scope ~poly ~kind ?hook obls
+  in ()
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 6c6da8952e..337da22018 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -15,8 +15,7 @@ open Constrexpr
 (** {6 Definitions/Let} *)
 
 val do_definition
-  :  program_mode:bool
-  -> ?hook:DeclareDef.Hook.t
+  :  ?hook:DeclareDef.Hook.t
   -> name:Id.t
   -> scope:DeclareDef.locality
   -> poly:bool
@@ -28,18 +27,15 @@ val do_definition
   -> constr_expr option
   -> unit
 
-(************************************************************************)
-(** Internal API  *)
-(************************************************************************)
-
-(** Not used anywhere. *)
-val interp_definition
-  :  program_mode:bool
+val do_definition_program
+  :  ?hook:DeclareDef.Hook.t
+  -> name:Id.t
+  -> scope:DeclareDef.locality
+  -> poly:bool
+  -> kind:Decls.definition_object_kind
   -> universe_decl_expr option
   -> local_binder_expr list
-  -> poly:bool
   -> red_expr option
   -> constr_expr
   -> constr_expr option
-  -> Evd.side_effects Declare.proof_entry *
-     Evd.evar_map * UState.universe_decl * Impargs.manual_implicits
+  -> unit
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index 6580495295..cbf0affc12 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -140,8 +140,8 @@ let compute_possible_guardness_evidences (ctx,_,recindex) =
          fixpoints ?) *)
       List.interval 0 (Context.Rel.nhyps ctx - 1)
 
-type recursive_preentry =
-  Id.t list * Sorts.relevance list * Constr.t option list * Constr.types list
+type ('constr, 'types) recursive_preentry =
+  Id.t list * Sorts.relevance list * 'constr option list * 'types list
 
 (* Wellfounded definition *)
 
@@ -230,7 +230,11 @@ let ground_fixpoint env evd (fixnames,fixrs,fixdefs,fixtypes) =
   let fixtypes = List.map EConstr.(to_constr evd) fixtypes in
   Evd.evar_universe_context evd, (fixnames,fixrs,fixdefs,fixtypes)
 
-let interp_fixpoint ~cofix l =
+(* XXX: Unify with interp_recursive  *)
+let interp_fixpoint ~cofix l :
+  ( (Constr.t, Constr.types) recursive_preentry *
+    UState.universe_decl * UState.t *
+    (EConstr.rel_context * Impargs.manual_implicits * int option) list) =
   let (env,_,pl,evd),fix,info = interp_recursive ~program_mode:false ~cofix l in
   check_recursive true env evd fix;
   let uctx,fix = ground_fixpoint env evd fix in
@@ -243,8 +247,10 @@ let build_recthms ~indexes fixnames fixtypes fiximps =
   in
   let thms =
     List.map3 (fun name typ (ctx,impargs,_) ->
-        { DeclareDef.Recthm.name; typ
-        ; args = List.map Context.Rel.Declaration.get_name ctx; impargs})
+        { DeclareDef.Recthm.name
+        ; typ
+        ; args = List.map Context.Rel.Declaration.get_name ctx
+        ; impargs})
       fixnames fixtypes fiximps
   in
   fix_kind, cofix, thms
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 2ad6c03bae..a19b96f0f3 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Names
-open Constr
 open Vernacexpr
 
 (** {6 Fixpoints and cofixpoints} *)
@@ -40,6 +39,9 @@ val adjust_rec_order
   -> Constrexpr.recursion_order_expr option
   -> lident option
 
+(** names / relevance / defs / types *)
+type ('constr, 'types) recursive_preentry = Id.t list * Sorts.relevance list * 'constr option list * 'types list
+
 (** Exported for Program *)
 val interp_recursive :
   (* Misc arguments *)
@@ -49,18 +51,17 @@ val interp_recursive :
   (* env / signature / univs / evar_map *)
   (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) *
   (* names / defs / types *)
-  (Id.t list * Sorts.relevance list * EConstr.constr option list * EConstr.types list) *
+  (EConstr.t, EConstr.types) recursive_preentry *
   (* ctx per mutual def / implicits / struct annotations *)
   (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
 (** Exported for Funind *)
 
-type recursive_preentry = Id.t list * Sorts.relevance list * constr option list * types list
-
 val interp_fixpoint
   :  cofix:bool
   -> lident option fix_expr_gen list
-  -> recursive_preentry * UState.universe_decl * UState.t *
+  -> (Constr.t, Constr.types) recursive_preentry *
+     UState.universe_decl * UState.t *
      (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
 (** Very private function, do not use *)
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 3bac0419ef..56780d00a6 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -254,9 +254,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
   in
   (* XXX: Capturing sigma here... bad bad *)
   let hook = DeclareDef.Hook.make (hook sigma) in
-  Obligations.check_evars env sigma;
+  RetrieveObl.check_evars env sigma;
   let evars, _, evars_def, evars_typ =
-    Obligations.eterm_obligations env recname sigma 0 def typ
+    RetrieveObl.retrieve_obligations env recname sigma 0 def typ
   in
   let uctx = Evd.evar_universe_context sigma in
   ignore(Obligations.add_definition ~name:recname ~term:evars_def ~udecl
@@ -281,15 +281,15 @@ let do_program_recursive ~scope ~poly fixkind fixl =
   let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in
     (* Solve remaining evars *)
   let evd = nf_evar_map_undefined evd in
-  let collect_evars id def typ imps =
+  let collect_evars name def typ impargs =
     (* Generalize by the recursive prototypes  *)
     let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in
     let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in
     let evm = collect_evars_of_term evd def typ in
     let evars, _, def, typ =
-      Obligations.eterm_obligations env id evm
+      RetrieveObl.retrieve_obligations env name evm
         (List.length rec_sign) def typ in
-    (id, def, typ, imps, evars)
+    ({ DeclareDef.Recthm.name; typ; impargs; args = [] }, def, evars)
   in
   let (fixnames,fixrs,fixdefs,fixtypes) = fix in
   let fiximps = List.map pi2 info in
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index fc53abdcea..1607771598 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Declare
-open Impargs
 
 type locality = Discharge | Global of Declare.import_status
 
@@ -34,41 +33,39 @@ module Hook = struct
 
   let make hook = CEphemeron.create hook
 
-  let call ?hook ?fix_exn x =
-    try Option.iter (fun hook -> CEphemeron.get hook x) hook
-    with e when CErrors.noncritical e ->
-      let e = Exninfo.capture e in
-      let e = Option.cata (fun fix -> fix e) e fix_exn in
-      Exninfo.iraise e
+  let call ?hook x = Option.iter (fun hook -> CEphemeron.get hook x) hook
+
 end
 
 (* Locality stuff *)
-let declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs ce =
-  let fix_exn = Declare.Internal.get_fix_exn ce in
-  let should_suggest = ce.Declare.proof_entry_opaque &&
-                       Option.is_empty ce.Declare.proof_entry_secctx in
+let declare_entry ~name ~scope ~kind ?hook ?(obls=[]) ~impargs ~uctx entry =
+  let should_suggest = entry.Declare.proof_entry_opaque &&
+                       Option.is_empty entry.Declare.proof_entry_secctx in
+  let ubind = UState.universe_binders uctx in
   let dref = match scope with
   | Discharge ->
-    let () = declare_variable ~name ~kind (SectionLocalDef ce) in
+    let () = declare_variable ~name ~kind (SectionLocalDef entry) in
     if should_suggest then Proof_using.suggest_variable (Global.env ()) name;
     Names.GlobRef.VarRef name
   | Global local ->
-    let kn = declare_constant ~name ~local ~kind (DefinitionEntry ce) in
+    let kn = declare_constant ~name ~local ~kind (DefinitionEntry entry) in
     let gr = Names.GlobRef.ConstRef kn in
     if should_suggest then Proof_using.suggest_constant (Global.env ()) kn;
     let () = DeclareUniv.declare_univ_binders gr ubind in
     gr
   in
-  let () = maybe_declare_manual_implicits false dref impargs in
+  let () = Impargs.maybe_declare_manual_implicits false dref impargs in
   let () = definition_message name in
-  begin
-    match hook_data with
-    | None -> ()
-    | Some (hook, uctx, obls) ->
-      Hook.call ~fix_exn ~hook { Hook.S.uctx; obls; scope; dref }
-  end;
+  Option.iter (fun hook -> Hook.call ~hook { Hook.S.uctx; obls; scope; dref }) hook;
   dref
 
+let declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry =
+  try declare_entry ~name ~scope ~kind ?hook ?obls ~impargs ~uctx entry
+  with exn ->
+    let exn = Exninfo.capture exn in
+    let fix_exn = Declare.Internal.get_fix_exn entry in
+    Exninfo.iraise (fix_exn exn)
+
 let mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes =
   match possible_indexes with
   | Some possible_indexes ->
@@ -98,22 +95,21 @@ end
 let declare_mutually_recursive ~opaque ~scope ~kind ~poly ~uctx ~udecl ~ntns ~rec_declaration ~possible_indexes ?(restrict_ucontext=true) fixitems =
   let vars, fixdecls, indexes =
     mutual_make_bodies ~fixitems ~rec_declaration ~possible_indexes in
-  let ubind, univs =
+  let uctx, univs =
     (* XXX: Obligations don't do this, this seems like a bug? *)
     if restrict_ucontext
     then
-      let evd = Evd.from_ctx uctx in
-      let evd = Evd.restrict_universe_context evd vars in
-      let univs = Evd.check_univ_decl ~poly evd udecl in
-      Evd.universe_binders evd, univs
+      let uctx = UState.restrict uctx vars in
+      let univs = UState.check_univ_decl ~poly uctx udecl in
+      uctx, univs
     else
       let univs = UState.univ_entry ~poly uctx in
-      UnivNames.empty_binders, univs
+      uctx, univs
   in
   let csts = CList.map2
       (fun Recthm.{ name; typ; impargs } body ->
-         let ce = Declare.definition_entry ~opaque ~types:typ ~univs body in
-         declare_definition ~name ~scope ~kind ~ubind ~impargs ce)
+         let entry = Declare.definition_entry ~opaque ~types:typ ~univs body in
+         declare_entry ~name ~scope ~kind ~impargs ~uctx entry)
       fixitems fixdecls
   in
   let isfix = Option.is_empty possible_indexes in
@@ -127,7 +123,7 @@ let warn_let_as_axiom =
     Pp.(fun id -> strbrk "Let definition" ++ spc () ++ Names.Id.print id ++
                   spc () ++ strbrk "declared as an axiom.")
 
-let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe =
+let declare_assumption ~name ~scope ~hook ~impargs ~uctx pe =
   let local = match scope with
     | Discharge -> warn_let_as_axiom name; Declare.ImportNeedQualified
     | Global local -> local
@@ -139,26 +135,58 @@ let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe =
   let () = Impargs.maybe_declare_manual_implicits false dref impargs in
   let () = Declare.assumption_message name in
   let () = DeclareUniv.declare_univ_binders dref (UState.universe_binders uctx) in
-  let () = Hook.(call ?fix_exn ?hook { S.uctx; obls = []; scope; dref}) in
+  let () = Hook.(call ?hook { S.uctx; obls = []; scope; dref}) in
   dref
 
+let declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe =
+  try declare_assumption ~name ~scope ~hook ~impargs ~uctx pe
+  with exn ->
+    let exn = Exninfo.capture exn in
+    let exn = Option.cata (fun fix -> fix exn) exn fix_exn in
+    Exninfo.iraise exn
+
 (* Preparing proof entries *)
 
-let check_definition_evars ~allow_evars sigma =
+let prepare_definition ?opaque ?inline ?fix_exn ~poly ~udecl ~types ~body sigma =
   let env = Global.env () in
-  if not allow_evars then Pretyping.check_evars_are_solved ~program_mode:false env sigma
+  Pretyping.check_evars_are_solved ~program_mode:false env sigma;
+  let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:true
+      sigma (fun nf -> nf body, Option.map nf types)
+  in
+  let univs = Evd.check_univ_decl ~poly sigma udecl in
+  let entry = definition_entry ?fix_exn ?opaque ?inline ?types ~univs body in
+  let uctx = Evd.evar_universe_context sigma in
+  entry, uctx
+
+let declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ?hook
+    ?obls ~poly ?inline ~types ~body ?fix_exn sigma =
+  let entry, uctx = prepare_definition ?fix_exn ~opaque ~poly ~udecl ~types ~body ?inline sigma in
+  declare_entry ~name ~scope ~kind ~impargs ?obls ?hook ~uctx entry
 
-let prepare_definition ~allow_evars ?opaque ?inline ~poly ~udecl ~types ~body sigma =
-  check_definition_evars ~allow_evars sigma;
-  let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
+let prepare_obligation ?opaque ?inline ~name ~poly ~udecl ~types ~body sigma =
+  let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false
       sigma (fun nf -> nf body, Option.map nf types)
   in
   let univs = Evd.check_univ_decl ~poly sigma udecl in
-  sigma, definition_entry ?opaque ?inline ?types ~univs body
+  let ce = definition_entry ?opaque ?inline ?types ~univs body in
+  let env = Global.env () in
+  let (c,ctx), sideff = Future.force ce.Declare.proof_entry_body in
+  assert(Safe_typing.empty_private_constants = sideff.Evd.seff_private);
+  assert(Univ.ContextSet.is_empty ctx);
+  RetrieveObl.check_evars env sigma;
+  let c = EConstr.of_constr c in
+  let typ = match ce.Declare.proof_entry_type with
+    | Some t -> EConstr.of_constr t
+    | None -> Retyping.get_type_of env sigma c
+  in
+  let obls, _, c, cty = RetrieveObl.retrieve_obligations env name sigma 0 c typ in
+  let uctx = Evd.evar_universe_context sigma in
+  c, cty, uctx, obls
 
-let prepare_parameter ~allow_evars ~poly ~udecl ~types sigma =
-  check_definition_evars ~allow_evars sigma;
-  let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:(not allow_evars)
+let prepare_parameter ~poly ~udecl ~types sigma =
+  let env = Global.env () in
+  Pretyping.check_evars_are_solved ~program_mode:false env sigma;
+  let sigma, typ = Evarutil.finalize ~abort_on_undefined_evars:true
       sigma (fun nf -> nf types)
   in
   let univs = Evd.check_univ_decl ~poly sigma udecl in
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index 1d7fd3a3bf..3bc1e25f19 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -36,19 +36,44 @@ module Hook : sig
   end
 
   val make : (S.t -> unit) -> t
-  val call : ?hook:t -> ?fix_exn:Future.fix_exn -> S.t -> unit
+  val call : ?hook:t -> S.t -> unit
 end
 
-val declare_definition
+(** Declare an interactively-defined constant *)
+val declare_entry
   :  name:Id.t
   -> scope:locality
   -> kind:Decls.logical_kind
-  -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
-  -> ubind:UnivNames.universe_binders
+  -> ?hook:Hook.t
+  -> ?obls:(Id.t * Constr.t) list
   -> impargs:Impargs.manual_implicits
+  -> uctx:UState.t
   -> Evd.side_effects Declare.proof_entry
   -> GlobRef.t
 
+(** Declares a non-interactive constant; [body] and [types] will be
+   normalized w.r.t. the passed [evar_map] [sigma]. Universes should
+   be handled properly, including minimization and restriction. Note
+   that [sigma] is checked for unresolved evars, thus you should be
+   careful not to submit open terms or evar maps with stale,
+   unresolved existentials *)
+val declare_definition
+  :  name:Id.t
+  -> scope:locality
+  -> kind:Decls.logical_kind
+  -> opaque:bool
+  -> impargs:Impargs.manual_implicits
+  -> udecl:UState.universe_decl
+  -> ?hook:Hook.t
+  -> ?obls:(Id.t * Constr.t) list
+  -> poly:bool
+  -> ?inline:bool
+  -> types:EConstr.t option
+  -> body:EConstr.t
+  -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
+  -> Evd.evar_map
+  -> GlobRef.t
+
 val declare_assumption
   :  ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
   -> name:Id.t
@@ -88,20 +113,19 @@ val declare_mutually_recursive
   -> Recthm.t list
   -> Names.GlobRef.t list
 
-val prepare_definition
-  :  allow_evars:bool
-  -> ?opaque:bool
+val prepare_obligation
+  :  ?opaque:bool
   -> ?inline:bool
+  -> name:Id.t
   -> poly:bool
   -> udecl:UState.universe_decl
   -> types:EConstr.t option
   -> body:EConstr.t
   -> Evd.evar_map
-  -> Evd.evar_map * Evd.side_effects Declare.proof_entry
+  -> Constr.constr * Constr.types * UState.t * RetrieveObl.obligation_info
 
 val prepare_parameter
-  : allow_evars:bool
-  -> poly:bool
+  : poly:bool
   -> udecl:UState.universe_decl
   -> types:EConstr.types
   -> Evd.evar_map
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index 98a9e4b9c9..bba3687256 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -362,34 +362,21 @@ let get_fix_exn, stm_get_fix_exn = Hook.make ()
 
 let declare_definition prg =
   let varsubst = obligation_substitution true prg in
-  let body, typ = subst_prog varsubst prg in
-  let nf =
-    UnivSubst.nf_evars_and_universes_opt_subst
-      (fun x -> None)
-      (UState.subst prg.prg_ctx)
-  in
-  let opaque = prg.prg_opaque in
+  let sigma = Evd.from_ctx prg.prg_ctx in
+  let body, types = subst_prog varsubst prg in
+  let body, types = EConstr.(of_constr body, Some (of_constr types)) in
+  (* All these should be grouped into a struct a some point *)
+  let opaque, poly, udecl, hook = prg.prg_opaque, prg.prg_poly, prg.prg_univdecl, prg.prg_hook in
+  let name, scope, kind, impargs = prg.prg_name, prg.prg_scope, Decls.(IsDefinition prg.prg_kind), prg.prg_implicits in
   let fix_exn = Hook.get get_fix_exn () in
-  let typ = nf typ in
-  let body = nf body in
-  let obls = List.map (fun (id, (_, c)) -> (id, nf c)) varsubst in
-  let uvars =
-    Univ.LSet.union
-      (Vars.universes_of_constr typ)
-      (Vars.universes_of_constr body)
-  in
-  let uctx = UState.restrict prg.prg_ctx uvars in
-  let univs =
-    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 obls = List.map (fun (id, (_, c)) -> (id, c)) varsubst in
+  (* XXX: This is doing normalization twice *)
   let () = progmap_remove prg in
-  let ubind = UState.universe_binders uctx in
-  let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in
-  DeclareDef.declare_definition
-    ~name:prg.prg_name ~scope:prg.prg_scope ~ubind
-    ~kind:Decls.(IsDefinition prg.prg_kind) ce
-    ~impargs:prg.prg_implicits ?hook_data
+  let kn =
+    DeclareDef.declare_definition ~name ~scope ~kind ~impargs ?hook ~obls
+      ~fix_exn ~opaque ~poly ~udecl ~types ~body sigma
+  in
+  kn
 
 let rec lam_index n t acc =
   match Constr.kind t with
@@ -464,9 +451,8 @@ let declare_mutual_definition l =
       ~restrict_ucontext:false fixitems
   in
   (* Only for the first constant *)
-  let fix_exn = Hook.get get_fix_exn () in
   let dref = List.hd kns in
-  DeclareDef.Hook.(call ?hook:first.prg_hook ~fix_exn { S.uctx = first.prg_ctx; obls; scope; dref });
+  DeclareDef.Hook.(call ?hook:first.prg_hook { S.uctx = first.prg_ctx; obls; scope; dref });
   List.iter progmap_remove l;
   dref
 
@@ -529,10 +515,6 @@ let obligation_terminator entries uctx { name; num; auto } =
     Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body);
     (* Declare the obligation ourselves and drop the hook *)
     let prg = CEphemeron.get (ProgMap.find name !from_prg) in
-    (* Ensure universes are substituted properly in body and type *)
-    let body = EConstr.to_constr sigma (EConstr.of_constr body) in
-    let ty = Option.map (fun x -> EConstr.to_constr sigma (EConstr.of_constr x)) ty in
-    let ctx = Evd.evar_universe_context sigma in
     let { obls; remaining=rem } = prg.prg_obligations in
     let obl = obls.(num) in
     let status =
@@ -545,24 +527,24 @@ let obligation_terminator entries uctx { name; num; auto } =
       | (_, status), false -> status
     in
     let obl = { obl with obl_status = false, status } in
-    let ctx =
-      if prg.prg_poly then ctx
-      else UState.union prg.prg_ctx ctx
+    let uctx =
+      if prg.prg_poly then uctx
+      else UState.union prg.prg_ctx uctx
     in
-    let uctx = UState.univ_entry ~poly:prg.prg_poly ctx in
-    let (defined, obl) = declare_obligation prg obl body ty uctx in
+    let univs = UState.univ_entry ~poly:prg.prg_poly uctx in
+    let (defined, obl) = declare_obligation prg obl body ty univs in
     let prg_ctx =
       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
+        UState.union prg.prg_ctx uctx
       else
         (* The first obligation, if defined,
            declares the univs of the constant,
            each subsequent obligation declares its own additional
            universes and constraints if any *)
         if defined then UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())
-        else ctx
+        else uctx
     in
     update_program_decl_on_defined prg obls num obl ~uctx:prg_ctx rem ~auto
   | _ ->
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index e08d2ce117..feedf4d71d 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -27,15 +27,12 @@ module Proof_ending = struct
     | Regular
     | End_obligation of DeclareObl.obligation_qed_info
     | End_derive of { f : Id.t; name : Id.t }
-    | End_equations of { hook : Constant.t list -> Evd.evar_map -> unit
-                       ; i : Id.t
-                       ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list
-                       ; wits : EConstr.t list ref
-                       (* wits are actually computed by the proof
-                          engine by side-effect after creating the
-                          proof! This is due to the start_dependent_proof API *)
-                       ; sigma : Evd.evar_map
-                       }
+    | End_equations of
+        { hook : Constant.t list -> Evd.evar_map -> unit
+        ; i : Id.t
+        ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list
+        ; sigma : Evd.evar_map
+        }
 
 end
 
@@ -43,22 +40,21 @@ 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 : DeclareDef.Recthm.t list
     ; scope : DeclareDef.locality
     ; kind : Decls.logical_kind
+    (* thms and compute guard are specific only to start_lemma_with_initialization + regular terminator *)
+    ; thms : DeclareDef.Recthm.t list
+    ; compute_guard : lemma_possible_guards
     }
 
   let make ?hook ?(proof_ending=Proof_ending.Regular) ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior)
       ?(kind=Decls.(IsProof Lemma)) () =
     { hook
     ; compute_guard = []
-    ; impargs = []
     ; proof_ending = CEphemeron.create proof_ending
-    ; other_thms = []
+    ; thms = []
     ; scope
     ; kind
     }
@@ -100,18 +96,30 @@ let initialize_named_context_for_proof () =
       let d = if Decls.variable_opacity id then NamedDecl.drop_body d else d in
       Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
 
+let add_first_thm ~info ~name ~typ ~impargs =
+  let thms =
+    { DeclareDef.Recthm.name
+    ; impargs
+    ; typ = EConstr.Unsafe.to_constr typ
+    ; args = [] } :: info.Info.thms
+  in
+  { info with Info.thms }
+
 (* Starting a goal *)
 let start_lemma ~name ~poly
     ?(udecl=UState.default_univ_decl)
-    ?(info=Info.make ())
-    sigma c =
+    ?(info=Info.make ()) ?(impargs=[]) sigma c =
   (* We remove the bodies of variables in the named context marked
      "opaque", this is a hack tho, see #10446 *)
   let sign = initialize_named_context_for_proof () in
   let goals = [ Global.env_of_context sign , c ] in
   let proof = Proof_global.start_proof sigma ~name ~udecl ~poly goals in
-  { proof ; info }
+  let info = add_first_thm ~info ~name ~typ:c ~impargs in
+  { proof; info }
 
+(* Note that proofs opened by start_dependent lemma cannot be closed
+   by the regular terminators, thus we don't need to update the [thms]
+   field. We will capture this invariant by typing in the future *)
 let start_dependent_lemma ~name ~poly
     ?(udecl=UState.default_univ_decl)
     ?(info=Info.make ()) telescope =
@@ -153,17 +161,18 @@ let start_lemma_with_initialization ?hook ~poly ~scope ~kind ~udecl sigma recgua
     intro_tac (List.hd thms), [] in
   match thms with
   | [] -> CErrors.anomaly (Pp.str "No proof to start.")
-  | { DeclareDef.Recthm.name; typ; impargs; _}::other_thms ->
+  | { DeclareDef.Recthm.name; typ; impargs; _} :: thms ->
     let info =
       Info.{ hook
-           ; impargs
            ; compute_guard
-           ; other_thms
            ; proof_ending = CEphemeron.create Proof_ending.Regular
+           ; thms
            ; scope
            ; kind
            } in
-    let lemma = start_lemma ~name ~poly ~udecl ~info sigma (EConstr.of_constr typ) in
+    (* start_lemma has the responsibility to add (name, impargs, typ)
+       to thms, once Info.t is more refined this won't be necessary *)
+    let lemma = start_lemma ~name ~impargs ~poly ~udecl ~info sigma (EConstr.of_constr typ) in
     pf_map (Proof_global.map_proof (fun p ->
         pi1 @@ Proof.run_tactic Global.(env ()) init_tac p)) lemma
 
@@ -179,39 +188,19 @@ module MutualEntry : sig
   val declare_variable
     : info:Info.t
     -> uctx:UState.t
-    (* Only for the first constant, introduced by compat *)
-    -> ubind:UnivNames.universe_binders
-    -> name:Id.t
     -> Entries.parameter_entry
     -> Names.GlobRef.t list
 
   val declare_mutdef
     (* Common to all recthms *)
     : info:Info.t
-    -> ?fix_exn:(Exninfo.iexn -> Exninfo.iexn)
     -> uctx:UState.t
-    -> ?hook_data:DeclareDef.Hook.t * UState.t * (Names.Id.t * Constr.t) list
-    (* Only for the first constant, introduced by compat *)
-    -> ubind:UnivNames.universe_binders
-    -> name:Id.t
     -> Evd.side_effects Declare.proof_entry
     -> Names.GlobRef.t list
 
 end = struct
 
-  (* Body with the fix *)
-  type et =
-    | NoBody of Entries.parameter_entry
-    | Single of Evd.side_effects Declare.proof_entry
-    | Mutual of Evd.side_effects Declare.proof_entry
-
-  type t =
-    { entry : et
-    ; info : Info.t
-    }
-
-  (* XXX: Refactor this with the code in
-     [ComFixpoint.declare_fixpoint_generic] *)
+  (* XXX: Refactor this with the code in [DeclareDef.declare_mutdef] *)
   let guess_decreasing env possible_indexes ((body, ctx), eff) =
     let open Constr in
     match Constr.kind body with
@@ -221,74 +210,55 @@ end = struct
       (mkFix ((indexes,0),fixdecls), ctx), eff
     | _ -> (body, ctx), eff
 
-  let adjust_guardness_conditions ~info const =
-    let entry = match info.Info.compute_guard with
-    | [] ->
-      (* Not a recursive statement *)
-      Single const
-    | possible_indexes ->
-      (* Try all combinations... not optimal *)
-      let env = Global.env() in
-      let pe = Declare.Internal.map_entry_body const
-          ~f:(guess_decreasing env possible_indexes)
-      in
-      Mutual pe
-    in { entry; info }
-
-  let rec select_body i t =
+  let select_body i t =
     let open Constr in
     match Constr.kind t with
     | Fix ((nv,0),decls) -> mkFix ((nv,i),decls)
     | CoFix (0,decls) -> mkCoFix (i,decls)
-    | LetIn(na,t1,ty,t2) -> mkLetIn (na,t1,ty, select_body i t2)
-    | Lambda(na,ty,t) -> mkLambda(na,ty, select_body i t)
-    | App (t, args) -> mkApp (select_body i t, args)
     | _ ->
       CErrors.anomaly
         Pp.(str "Not a proof by induction: " ++
             Termops.Internal.debug_print_constr (EConstr.of_constr t) ++ str ".")
 
-  let declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind ~name ?typ ~impargs ~info mutpe i =
-    let { Info.hook; compute_guard; scope; kind; _ } = info in
-    match mutpe with
-    | NoBody pe ->
-      DeclareDef.declare_assumption ?fix_exn ~name ~scope ~hook ~impargs ~uctx pe
-    | Single pe ->
-      (* We'd like to do [assert (i = 0)] here, however this codepath
-         is used when declaring mutual cofixpoints *)
-      DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe
-    | Mutual pe ->
-      (* if typ = None , we don't touch the type; used in the base case *)
-      let pe =
-        match typ with
-        | None -> pe
-        | Some typ ->
-          Declare.Internal.map_entry_type pe ~f:(fun _ -> Some typ)
-      in
-      let pe = Declare.Internal.map_entry_body pe
-          ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff) in
-      DeclareDef.declare_definition ~name ~scope ~kind ?hook_data ~ubind ~impargs pe
-
-  let declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind ~name { entry; info } =
-    (* At some point make this a single iteration *)
-    (* At some point make this a single iteration *)
-    (* impargs here are special too, fixed in upcoming PRs *)
-    let impargs = info.Info.impargs in
-    let r = declare_mutdef ?fix_exn ~info ~ubind ?hook_data ~uctx ~name ~impargs entry 0 in
-    (* Before we used to do this, check if that's right *)
-    let ubind = UnivNames.empty_binders in
-    let rs =
-      List.map_i (
-        fun i { DeclareDef.Recthm.name; typ; impargs } ->
-          declare_mutdef ?fix_exn ~name ~info ~ubind ?hook_data ~uctx ~typ ~impargs entry i) 1 info.Info.other_thms
-    in r :: rs
-
-  let declare_variable ~info ~uctx ~ubind ~name pe =
-    declare_mutdef ~uctx ~ubind ~name { entry = NoBody pe; info }
-
-  let declare_mutdef ~info ?fix_exn ~uctx ?hook_data ~ubind ~name const =
-    let mutpe = adjust_guardness_conditions ~info const in
-    declare_mutdef ?fix_exn ~uctx ?hook_data ~ubind ~name mutpe
+  let declare_mutdef ~uctx ~info pe i DeclareDef.Recthm.{ name; impargs; typ; _} =
+    let { Info.hook; scope; kind; compute_guard; _ } = info in
+    (* if i = 0 , we don't touch the type; this is for compat
+       but not clear it is the right thing to do.
+    *)
+    let pe, ubind =
+      if i > 0 && not (CList.is_empty compute_guard)
+      then Declare.Internal.map_entry_type pe ~f:(fun _ -> Some typ), UnivNames.empty_binders
+      else pe, UState.universe_binders uctx
+    in
+    (* We when compute_guard was [] in the previous step we should not
+       substitute the body *)
+    let pe = match compute_guard with
+      | [] -> pe
+      | _ ->
+        Declare.Internal.map_entry_body pe
+          ~f:(fun ((body, ctx), eff) -> (select_body i body, ctx), eff)
+    in
+    DeclareDef.declare_entry ~name ~scope ~kind ?hook ~impargs ~uctx pe
+
+  let declare_mutdef ~info ~uctx const =
+    let pe = match info.Info.compute_guard with
+    | [] ->
+      (* Not a recursive statement *)
+      const
+    | possible_indexes ->
+      (* Try all combinations... not optimal *)
+      let env = Global.env() in
+      Declare.Internal.map_entry_body const
+        ~f:(guess_decreasing env possible_indexes)
+    in
+    List.map_i (declare_mutdef ~info ~uctx pe) 0 info.Info.thms
+
+  let declare_variable ~info ~uctx pe =
+    let { Info.scope; hook } = info in
+    List.map_i (
+      fun i { DeclareDef.Recthm.name; typ; impargs } ->
+        DeclareDef.declare_assumption ~name ~scope ~hook ~impargs ~uctx pe
+    ) 0 info.Info.thms
 
 end
 
@@ -316,14 +286,13 @@ let compute_proof_using_for_admitted proof typ pproofs =
       Some (Environ.really_needed env (Id.Set.union ids_typ ids_def))
     | _ -> None
 
-let finish_admitted ~name ~info ~uctx pe =
-  let ubind = UnivNames.empty_binders in
-  let _r : Names.GlobRef.t list = MutualEntry.declare_variable ~info ~uctx ~ubind ~name pe in
+let finish_admitted ~info ~uctx pe =
+  let _r : Names.GlobRef.t list = MutualEntry.declare_variable ~info ~uctx pe in
   ()
 
 let save_lemma_admitted ~(lemma : t) : unit =
   let udecl = Proof_global.get_universe_decl lemma.proof in
-  let Proof.{ name; poly; entry } = Proof.data (Proof_global.get_proof lemma.proof) in
+  let Proof.{ poly; entry } = Proof.data (Proof_global.get_proof lemma.proof) in
   let typ = match Proofview.initial_goals entry with
     | [typ] -> snd typ
     | _ -> CErrors.anomaly ~label:"Lemmas.save_lemma_admitted" (Pp.str "more than one statement.")
@@ -332,48 +301,26 @@ let save_lemma_admitted ~(lemma : t) : unit =
   let proof = Proof_global.get_proof lemma.proof in
   let pproofs = Proof.partial_proof proof in
   let sec_vars = compute_proof_using_for_admitted lemma.proof typ pproofs in
-  let universes = Proof_global.get_initial_euctx lemma.proof in
-  let ctx = UState.check_univ_decl ~poly universes udecl in
-  finish_admitted ~name ~info:lemma.info ~uctx:universes (sec_vars, (typ, ctx), None)
+  let uctx = Proof_global.get_initial_euctx lemma.proof in
+  let univs = UState.check_univ_decl ~poly uctx udecl in
+  finish_admitted ~info:lemma.info ~uctx (sec_vars, (typ, univs), None)
 
 (************************************************************************)
 (* Saving a lemma-like constant                                         *)
 (************************************************************************)
 
-let default_thm_id = Id.of_string "Unnamed_thm"
-
-let check_anonymity id save_ident =
-  if not (String.equal (Nameops.atompart_of_id id) (Id.to_string (default_thm_id))) then
-    CErrors.user_err Pp.(str "This command can only be used for unnamed theorem.")
-
-let finish_proved idopt po info =
+let finish_proved po info =
   let open Proof_global in
-  let { Info.hook } = info in
   match po with
-  | { name; entries=[const]; uctx; udecl } ->
-    let name = match idopt with
-      | None -> name
-      | Some { CAst.v = save_id } -> check_anonymity name save_id; save_id in
-    let fix_exn = Declare.Internal.get_fix_exn const in
-    let () = try
-      let hook_data = Option.map (fun hook -> hook, uctx, []) hook in
-      let ubind = UState.universe_binders uctx in
-      let _r : Names.GlobRef.t list =
-        MutualEntry.declare_mutdef ~info ~fix_exn ~uctx ?hook_data ~ubind ~name const
-      in ()
-    with e when CErrors.noncritical e ->
-      let e = Exninfo.capture e in
-      Exninfo.iraise (fix_exn e)
-    in ()
+  | { entries=[const]; uctx } ->
+    let _r : Names.GlobRef.t list = MutualEntry.declare_mutdef ~info ~uctx const in
+    ()
   | _ ->
     CErrors.anomaly ~label:"finish_proved" Pp.(str "close_proof returned more than one proof term")
 
-let finish_derived ~f ~name ~idopt ~entries =
+let finish_derived ~f ~name ~entries =
   (* [f] and [name] correspond to the proof of [f] and of [suchthat], respectively. *)
 
-  if Option.has_some idopt then
-    CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.");
-
   let f_def, lemma_def =
     match entries with
     | [_;f_def;lemma_def] ->
@@ -406,11 +353,11 @@ let finish_derived ~f ~name ~idopt ~entries =
   let _ : Names.Constant.t = Declare.declare_constant ~name ~kind:Decls.(IsProof Proposition) lemma_def in
   ()
 
-let finish_proved_equations lid kind proof_obj hook i types wits sigma0 =
+let finish_proved_equations ~kind ~hook i proof_obj types sigma0 =
 
   let obls = ref 1 in
   let sigma, recobls =
-    CList.fold_left2_map (fun sigma (wit, (evar_env, ev, evi, local_context, type_)) entry ->
+    CList.fold_left2_map (fun sigma (_evar_env, ev, _evi, local_context, _type) entry ->
         let id =
           match Evd.evar_ident ev sigma0 with
           | Some id -> id
@@ -421,34 +368,51 @@ let finish_proved_equations lid kind proof_obj hook i types wits sigma0 =
         let sigma, app = Evarutil.new_global sigma (GlobRef.ConstRef cst) in
         let sigma = Evd.define ev (EConstr.applist (app, List.map EConstr.of_constr args)) sigma in
         sigma, cst) sigma0
-      (CList.combine (List.rev !wits) types) proof_obj.Proof_global.entries
+      types proof_obj.Proof_global.entries
   in
   hook recobls sigma
 
-let finalize_proof idopt proof_obj proof_info =
+let finalize_proof proof_obj proof_info =
   let open Proof_global in
   let open Proof_ending in
   match CEphemeron.default proof_info.Info.proof_ending Regular with
   | Regular ->
-    finish_proved idopt proof_obj proof_info
+    finish_proved proof_obj proof_info
   | End_obligation oinfo ->
     DeclareObl.obligation_terminator proof_obj.entries proof_obj.uctx oinfo
   | End_derive { f ; name } ->
-    finish_derived ~f ~name ~idopt ~entries:proof_obj.entries
-  | End_equations { hook; i; types; wits; sigma } ->
-    finish_proved_equations idopt proof_info.Info.kind proof_obj hook i types wits sigma
+    finish_derived ~f ~name ~entries:proof_obj.entries
+  | End_equations { hook; i; types; sigma } ->
+    finish_proved_equations ~kind:proof_info.Info.kind ~hook i proof_obj types sigma
+
+let err_save_forbidden_in_place_of_qed () =
+  CErrors.user_err (Pp.str "Cannot use Save with more than one constant or in this proof mode")
+
+let process_idopt_for_save ~idopt info =
+  match idopt with
+  | None -> info
+  | Some { CAst.v = save_name } ->
+    (* Save foo was used; we override the info in the first theorem *)
+    let thms =
+      match info.Info.thms, CEphemeron.default info.Info.proof_ending Proof_ending.Regular with
+      | [ { DeclareDef.Recthm.name; _} as decl ], Proof_ending.Regular ->
+        [ { decl with DeclareDef.Recthm.name = save_name } ]
+      | _ ->
+        err_save_forbidden_in_place_of_qed ()
+    in { info with Info.thms }
 
 let save_lemma_proved ~lemma ~opaque ~idopt =
   (* Env and sigma are just used for error printing in save_remaining_recthms *)
   let proof_obj = Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) lemma.proof in
-  finalize_proof idopt proof_obj lemma.info
+  let proof_info = process_idopt_for_save ~idopt lemma.info in
+  finalize_proof proof_obj proof_info
 
 (***********************************************************************)
 (* Special case to close a lemma without forcing a proof               *)
 (***********************************************************************)
 let save_lemma_admitted_delayed ~proof ~info =
   let open Proof_global in
-  let { name; entries; uctx; udecl } = proof in
+  let { entries; uctx } = proof in
   if List.length entries <> 1 then
     CErrors.user_err Pp.(str "Admitted does not support multiple statements");
   let { Declare.proof_entry_secctx; proof_entry_type; proof_entry_universes } = List.hd entries in
@@ -460,6 +424,14 @@ let save_lemma_admitted_delayed ~proof ~info =
     | Some typ -> typ in
   let ctx = UState.univ_entry ~poly uctx in
   let sec_vars = if get_keep_admitted_vars () then proof_entry_secctx else None in
-  finish_admitted ~name ~uctx ~info (sec_vars, (typ, ctx), None)
-
-let save_lemma_proved_delayed ~proof ~info ~idopt = finalize_proof idopt proof info
+  finish_admitted ~uctx ~info (sec_vars, (typ, ctx), None)
+
+let save_lemma_proved_delayed ~proof ~info ~idopt =
+  (* vio2vo calls this but with invalid info, we have to workaround
+     that to add the name to the info structure *)
+  if CList.is_empty info.Info.thms then
+    let info = add_first_thm ~info ~name:proof.Proof_global.name ~typ:EConstr.mkSet ~impargs:[] in
+    finalize_proof proof info
+  else
+    let info = process_idopt_for_save ~idopt info in
+    finalize_proof proof info
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 6a1f8c09f3..8a23daa85f 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -35,12 +35,12 @@ module Proof_ending : sig
     | Regular
     | End_obligation of DeclareObl.obligation_qed_info
     | End_derive of { f : Id.t; name : Id.t }
-    | End_equations of { hook : Constant.t list -> Evd.evar_map -> unit
-                       ; i : Id.t
-                       ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list
-                       ; wits : EConstr.t list ref
-                       ; sigma : Evd.evar_map
-                       }
+    | End_equations of
+        { hook : Constant.t list -> Evd.evar_map -> unit
+        ; i : Id.t
+        ; types : (Environ.env * Evar.t * Evd.evar_info * EConstr.named_context * Evd.econstr) list
+        ; sigma : Evd.evar_map
+        }
 
 end
 
@@ -68,6 +68,7 @@ val start_lemma
   -> poly:bool
   -> ?udecl:UState.universe_decl
   -> ?info:Info.t
+  -> ?impargs:Impargs.manual_implicits
   -> Evd.evar_map
   -> EConstr.types
   -> t
@@ -95,8 +96,6 @@ val start_lemma_with_initialization
   -> int list option
   -> t
 
-val default_thm_id : Names.Id.t
-
 (** {4 Saving proofs} *)
 
 val save_lemma_admitted : lemma:t -> unit
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index a29ba44907..435085793c 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -10,252 +10,16 @@
 
 open Printf
 
-(**
-   - Get types of existentials ;
-   - Flatten dependency tree (prefix order) ;
-   - Replace existentials by de Bruijn indices in term, applied to the right arguments ;
-   - Apply term prefixed by quantification on "existentials".
-*)
-
-open Constr
 open Names
 open Pp
 open CErrors
 open Util
 
-module NamedDecl = Context.Named.Declaration
-
 (* For the records fields, opens should go away one these types are private *)
 open DeclareObl
 open DeclareObl.Obligation
 open DeclareObl.ProgramDecl
 
-let succfix (depth, fixrels) =
-  (succ depth, List.map succ fixrels)
-
-let check_evars env evm =
-  Evar.Map.iter
-    (fun key evi ->
-       if Evd.is_obligation_evar evm key then ()
-       else
-         let (loc,k) = Evd.evar_source key evm in
-         Pretype_errors.error_unsolvable_implicit ?loc env evm key None)
-  (Evd.undefined_map evm)
-
-type oblinfo =
-  { ev_name: int * Id.t;
-    ev_hyps: EConstr.named_context;
-    ev_status: bool * Evar_kinds.obligation_definition_status;
-    ev_chop: int option;
-    ev_src: Evar_kinds.t Loc.located;
-    ev_typ: types;
-    ev_tac: unit Proofview.tactic option;
-    ev_deps: Int.Set.t }
-
-(** Substitute evar references in t using de Bruijn indices,
-  where n binders were passed through. *)
-
-let subst_evar_constr evm evs n idf t =
-  let seen = ref Int.Set.empty in
-  let transparent = ref Id.Set.empty in
-  let evar_info id = List.assoc_f Evar.equal id evs in
-  let rec substrec (depth, fixrels) c = match EConstr.kind evm c with
-    | Evar (k, args) ->
-        let { ev_name = (id, idstr) ;
-              ev_hyps = hyps ; ev_chop = chop } =
-          try evar_info k
-          with Not_found ->
-            anomaly ~label:"eterm" (Pp.str "existential variable " ++ int (Evar.repr k) ++ str " not found.")
-        in
-        seen := Int.Set.add id !seen;
-          (* Evar arguments are created in inverse order,
-             and we must not apply to defined ones (i.e. LetIn's)
-          *)
-        let args =
-          let n = match chop with None -> 0 | Some c -> c in
-          let (l, r) = List.chop n (List.rev (Array.to_list args)) in
-            List.rev r
-        in
-        let args =
-          let rec aux hyps args acc =
-             let open Context.Named.Declaration in
-             match hyps, args with
-                 (LocalAssum _ :: tlh), (c :: tla) ->
-                   aux tlh tla ((substrec (depth, fixrels) c) :: acc)
-               | (LocalDef _ :: tlh), (_ :: tla) ->
-                   aux tlh tla acc
-               | [], [] -> acc
-               | _, _ -> acc (*failwith "subst_evars: invalid argument"*)
-          in aux hyps args []
-        in
-          if List.exists
-            (fun x -> match EConstr.kind evm x with
-            | Rel n -> Int.List.mem n fixrels
-            | _ -> false) args
-          then
-            transparent := Id.Set.add idstr !transparent;
-          EConstr.mkApp (idf idstr, Array.of_list args)
-    | Fix _ ->
-        EConstr.map_with_binders evm succfix substrec (depth, 1 :: fixrels) c
-    | _ -> EConstr.map_with_binders evm succfix substrec (depth, fixrels) c
-  in
-  let t' = substrec (0, []) t in
-    EConstr.to_constr evm t', !seen, !transparent
-
-
-(** Substitute variable references in t using de Bruijn indices,
-  where n binders were passed through. *)
-let subst_vars acc n t =
-  let var_index id = Util.List.index Id.equal id acc in
-  let rec substrec depth c = match Constr.kind c with
-    | Var v -> (try mkRel (depth + (var_index v)) with Not_found -> c)
-    | _ -> Constr.map_with_binders succ substrec depth c
-  in
-    substrec 0 t
-
-(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ])
-    to a product : forall H1 : t1, ..., forall Hn : tn, concl.
-    Changes evars and hypothesis references to variable references.
-*)
-let etype_of_evar evm evs hyps concl =
-  let open Context.Named.Declaration in
-  let rec aux acc n = function
-      decl :: tl ->
-        let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar (NamedDecl.get_type decl) in
-        let t'' = subst_vars acc 0 t' in
-        let rest, s', trans' = aux (NamedDecl.get_id decl :: acc) (succ n) tl in
-        let s' = Int.Set.union s s' in
-        let trans' = Id.Set.union trans trans' in
-          (match decl with
-            | LocalDef (id,c,_) ->
-                let c', s'', trans'' = subst_evar_constr evm evs n EConstr.mkVar c in
-                let c' = subst_vars acc 0 c' in
-                Term.mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest,
-                Int.Set.union s'' s',
-                Id.Set.union trans'' trans'
-            | LocalAssum (id,_) ->
-              Term.mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans')
-    | [] ->
-      let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in
-      subst_vars acc 0 t', s, trans
-  in aux [] 0 (List.rev hyps)
-
-let trunc_named_context n ctx =
-  let len = List.length ctx in
-    List.firstn (len - n) ctx
-
-let rec chop_product n t =
-  let pop t = Vars.lift (-1) t in
-  if Int.equal n 0 then Some t
-  else
-    match Constr.kind t with
-      | Prod (_, _, b) ->  if Vars.noccurn 1 b then chop_product (pred n) (pop b) else None
-      | _ -> None
-
-let evar_dependencies evm oev =
-  let one_step deps =
-    Evar.Set.fold (fun ev s ->
-      let evi = Evd.find evm ev in
-      let deps' = Evd.evars_of_filtered_evar_info evm evi in
-      if Evar.Set.mem oev deps' then
-        invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ Pp.string_of_ppcmds @@ Evar.print oev)
-      else Evar.Set.union deps' s)
-      deps deps
-  in
-  let rec aux deps =
-    let deps' = one_step deps in
-      if Evar.Set.equal deps deps' then deps
-      else aux deps'
-  in aux (Evar.Set.singleton oev)
-
-let move_after (id, ev, deps as obl) l =
-  let rec aux restdeps = function
-    | (id', _, _) as obl' :: tl ->
-        let restdeps' = Evar.Set.remove id' restdeps in
-          if Evar.Set.is_empty restdeps' then
-            obl' :: obl :: tl
-          else obl' :: aux restdeps' tl
-    | [] -> [obl]
-  in aux (Evar.Set.remove id deps) l
-
-let sort_dependencies evl =
-  let rec aux l found list =
-    match l with
-    | (id, ev, deps) as obl :: tl ->
-        let found' = Evar.Set.union found (Evar.Set.singleton id) in
-          if Evar.Set.subset deps found' then
-            aux tl found' (obl :: list)
-          else aux (move_after obl tl) found list
-    | [] -> List.rev list
-  in aux evl Evar.Set.empty []
-
-let eterm_obligations env name evm fs ?status t ty =
-  (* 'Serialize' the evars *)
-  let nc = Environ.named_context env in
-  let nc_len = Context.Named.length nc in
-  let evm = Evarutil.nf_evar_map_undefined evm in
-  let evl = Evarutil.non_instantiated evm in
-  let evl = Evar.Map.bindings evl in
-  let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in
-  let sevl = sort_dependencies evl in
-  let evl = List.map (fun (id, ev, _) -> id, ev) sevl in
-  let evn =
-    let i = ref (-1) in
-      List.rev_map (fun (id, ev) -> incr i;
-                      (id, (!i, Id.of_string
-                              (Id.to_string name ^ "_obligation_" ^ string_of_int (succ !i))),
-                       ev)) evl
-  in
-  let evts =
-    (* Remove existential variables in types and build the corresponding products *)
-    List.fold_right
-      (fun (id, (n, nstr), ev) l ->
-         let hyps = Evd.evar_filtered_context ev in
-         let hyps = trunc_named_context nc_len hyps in
-         let evtyp, deps, transp = etype_of_evar evm l hyps ev.Evd.evar_concl in
-         let evtyp, hyps, chop =
-           match chop_product fs evtyp with
-           | Some t -> t, trunc_named_context fs hyps, fs
-           | None -> evtyp, hyps, 0
-         in
-         let loc, k = Evd.evar_source id evm in
-         let status = match k with
-           | Evar_kinds.QuestionMark { Evar_kinds.qm_obligation=o } -> o
-           | _ -> match status with
-                 | Some o -> o
-                 | None -> Evar_kinds.Define (not (Program.get_proofs_transparency ()))
-         in
-         let force_status, status, chop = match status with
-           | Evar_kinds.Define true as stat ->
-              if not (Int.equal chop fs) then true, Evar_kinds.Define false, None
-              else false, stat, Some chop
-           | s -> false, s, None
-         in
-         let info = { ev_name = (n, nstr);
-                      ev_hyps = hyps; ev_status = force_status, status; ev_chop = chop;
-                      ev_src = loc, k; ev_typ = evtyp ; ev_deps = deps; ev_tac = None }
-         in (id, info) :: l)
-      evn []
-  in
-  let t', _, transparent = (* Substitute evar refs in the term by variables *)
-    subst_evar_constr evm evts 0 EConstr.mkVar t
-  in
-  let ty, _, _ = subst_evar_constr evm evts 0 EConstr.mkVar ty in
-  let evars =
-    List.map (fun (ev, info) ->
-      let { ev_name = (_, name); ev_status = force_status, status;
-            ev_src = src; ev_typ = typ; ev_deps = deps; ev_tac = tac } = info
-      in
-      let force_status, status = match status with
-        | Evar_kinds.Define true when Id.Set.mem name transparent ->
-          true, Evar_kinds.Define false
-        | _ -> force_status, status
-      in name, typ, src, (force_status, status), deps, tac) evts
-  in
-  let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in
-  let evmap f c = pi1 (subst_evar_constr evm evts 0 f c) in
-    Array.of_list (List.rev evars), (evnames, evmap), t', ty
-
 let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
 let error s = pperror (str s)
 
@@ -270,11 +34,6 @@ let explain_no_obligations = function
     Some ident -> str "No obligations for program " ++ Id.print ident
   | None -> str "No obligations remaining"
 
-type obligation_info =
-    (Names.Id.t * types * Evar_kinds.t Loc.located *
-       (bool * Evar_kinds.obligation_definition_status)
-       * Int.Set.t * unit Proofview.tactic option) array
-
 let assumption_message = Declare.assumption_message
 
 let default_tactic = ref (Proofview.tclUNIT ())
@@ -571,12 +330,12 @@ let add_definition ~name ?term t ~uctx ?(udecl=UState.default_univ_decl)
 let add_mutual_definitions l ~uctx ?(udecl=UState.default_univ_decl) ?tactic
                            ~poly ?(scope=DeclareDef.Global Declare.ImportDefaultBehavior) ?(kind=Decls.Definition) ?(reduce=reduce)
     ?hook ?(opaque = false) notations fixkind =
-  let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
+  let deps = List.map (fun ({ DeclareDef.Recthm.name; _ }, _, _) -> name) l in
     List.iter
-    (fun  (n, b, t, impargs, obls) ->
-     let prg = ProgramDecl.make ~opaque n ~udecl (Some b) t ~uctx deps (Some fixkind)
+    (fun ({ DeclareDef.Recthm.name; typ; impargs; _ }, b, obls) ->
+     let prg = ProgramDecl.make ~opaque name ~udecl (Some b) typ ~uctx deps (Some fixkind)
        notations obls ~impargs ~poly ~scope ~kind reduce ?hook
-     in progmap_add n (CEphemeron.create prg)) l;
+     in progmap_add name (CEphemeron.create prg)) l;
     let _defined =
       List.fold_left (fun finished x ->
         if finished then finished
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 101958072a..f42d199e18 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -8,51 +8,73 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Environ
 open Constr
-open Evd
-open Names
-
-val check_evars : env -> evar_map -> unit
-
-val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t
-val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar_info * Evar.Set.t) list
-
-(* ident, type, location, (opaque or transparent, expand or define), dependencies, tactic to solve it *)
-type obligation_info =
-  (Id.t * types * Evar_kinds.t Loc.located *
-   (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array
-
-(* env, id, evars, number of function prototypes to try to clear from
-   evars contexts, object and type *)
-val eterm_obligations
-  :  env
-  -> Id.t
-  -> evar_map
-  -> int
-  -> ?status:Evar_kinds.obligation_definition_status
-  -> EConstr.constr
-  -> EConstr.types
-  -> obligation_info *
-
-     (* Existential key, obl. name, type as product, location of the
-        original evar, associated tactic, status and dependencies as
-        indexes into the array *)
-     ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) *
-
-     (* Translations from existential identifiers to obligation
-        identifiers and for terms with existentials to closed terms,
-        given a translation from obligation identifiers to constrs,
-        new term, new type *)
-     constr * types
+
+(** Coq's Program mode support. This mode extends declarations of
+   constants and fixpoints with [Program Definition] and [Program
+   Fixpoint] to support incremental construction of terms using
+   delayed proofs, called "obligations"
+
+    The mode also provides facilities for managing and auto-solving
+   sets of obligations.
+
+    The basic code flow of programs/obligations is as follows:
+
+    - [add_definition] / [add_mutual_definitions] are called from the
+   respective [Program] vernacular command interpretation; at this
+   point the only extra work we do is to prepare the new definition
+   [d] using [RetrieveObl], which consists in turning unsolved evars
+   into obligations. [d] is not sent to the kernel yet, as it is not
+   complete and cannot be typchecked, but saved in a special
+   data-structure. Auto-solving of obligations is tried at this stage
+   (see below)
+
+   - [next_obligation] will retrieve the next obligation
+   ([RetrieveObl] sorts them by topological order) and will try to
+   solve it. When all obligations are solved, the original constant
+   [d] is grounded and sent to the kernel for addition to the global
+   environment. Auto-solving of obligations is also triggered on
+   obligation completion.
+
+{2} Solving of obligations: Solved obligations are stored as regular
+   global declarations in the global environment, usually with name
+   [constant_obligation_number] where [constant] is the original
+   [constant] and [number] is the corresponding (internal) number.
+
+   Solving an obligation can trigger a bit of a complex cascaded
+   callback path; closing an obligation can indeed allow all other
+   obligations to be closed, which in turn may trigged the declaration
+   of the original constant. Care must be taken, as this can modify
+   [Global.env] in arbitrarily ways. Current code takes some care to
+   refresh the [env] in the proper boundaries, but the invariants
+   remain delicate.
+
+{2} Saving of obligations: as open obligations use the regular proof
+   mode, a `Qed` will call `Lemmas.save_lemma` first. For this reason
+   obligations code is split in two: this file, [Obligations], taking
+   care of the top-level vernac commands, and [DeclareObl], which is
+   called by `Lemmas` to close an obligation proof and eventually to
+   declare the top-level [Program]ed constant.
+
+    There is little obligations-specific code in [DeclareObl], so
+   eventually that file should be integrated in the regular [Declare]
+   path, as it gains better support for "dependent_proofs".
+
+ *)
 
 val default_tactic : unit Proofview.tactic ref
 
-val add_definition
-  :  name:Names.Id.t
-  -> ?term:constr -> types
+(** Start a [Program Definition c] proof. [uctx] [udecl] [impargs]
+   [kind] [scope] [poly] etc... come from the interpretation of the
+   vernacular; `obligation_info` was generated by [RetrieveObl] It
+   will return whether all the obligations were solved; if so, it will
+   also register [c] with the kernel. *)
+val add_definition :
+     name:Names.Id.t
+  -> ?term:constr
+  -> types
   -> uctx:UState.t
-  -> ?udecl:UState.universe_decl (* Universe binders and constraints *)
+  -> ?udecl:UState.universe_decl (** Universe binders and constraints *)
   -> ?impargs:Impargs.manual_implicits
   -> poly:bool
   -> ?scope:DeclareDef.locality
@@ -61,52 +83,56 @@ val add_definition
   -> ?reduce:(constr -> constr)
   -> ?hook:DeclareDef.Hook.t
   -> ?opaque:bool
-  -> obligation_info
+  -> RetrieveObl.obligation_info
   -> DeclareObl.progress
 
-val add_mutual_definitions
-  (* XXX: unify with MutualEntry *)
-  : (Names.Id.t * constr * types * Impargs.manual_implicits * obligation_info) list
+(* XXX: unify with MutualEntry *)
+
+(** Start a [Program Fixpoint] declaration, similar to the above,
+   except it takes a list now. *)
+val add_mutual_definitions :
+     (DeclareDef.Recthm.t * Constr.t * RetrieveObl.obligation_info) list
   -> uctx:UState.t
-  -> ?udecl:UState.universe_decl
-  (** Universe binders and constraints *)
+  -> ?udecl:UState.universe_decl (** Universe binders and constraints *)
   -> ?tactic:unit Proofview.tactic
   -> poly:bool
   -> ?scope:DeclareDef.locality
   -> ?kind:Decls.definition_object_kind
   -> ?reduce:(constr -> constr)
-  -> ?hook:DeclareDef.Hook.t -> ?opaque:bool
+  -> ?hook:DeclareDef.Hook.t
+  -> ?opaque:bool
   -> Vernacexpr.decl_notation list
-  -> DeclareObl.fixpoint_kind -> unit
+  -> DeclareObl.fixpoint_kind
+  -> unit
 
-val obligation
-  :  int * Names.Id.t option * Constrexpr.constr_expr option
+(** Implementation of the [Obligation] command *)
+val obligation :
+     int * Names.Id.t option * Constrexpr.constr_expr option
   -> Genarg.glob_generic_argument option
   -> Lemmas.t
 
-val next_obligation
-  :  Names.Id.t option
-  -> Genarg.glob_generic_argument option
-  -> Lemmas.t
+(** Implementation of the [Next Obligation] command *)
+val next_obligation :
+  Names.Id.t option -> Genarg.glob_generic_argument option -> Lemmas.t
 
-val solve_obligations : Names.Id.t option -> unit Proofview.tactic option
-  -> DeclareObl.progress
-(* Number of remaining obligations to be solved for this program *)
+(** Implementation of the [Solve Obligation] command *)
+val solve_obligations :
+  Names.Id.t option -> unit Proofview.tactic option -> DeclareObl.progress
 
 val solve_all_obligations : unit Proofview.tactic option -> unit
 
-val try_solve_obligation : int -> Names.Id.t option -> unit Proofview.tactic option -> unit
+(** Number of remaining obligations to be solved for this program *)
+val try_solve_obligation :
+  int -> Names.Id.t option -> unit Proofview.tactic option -> unit
 
-val try_solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> unit
+val try_solve_obligations :
+  Names.Id.t option -> unit Proofview.tactic option -> unit
 
 val show_obligations : ?msg:bool -> Names.Id.t option -> unit
-
 val show_term : Names.Id.t option -> Pp.t
-
 val admit_obligations : Names.Id.t option -> unit
 
 exception NoObligations of Names.Id.t option
 
 val explain_no_obligations : Names.Id.t option -> Pp.t
-
 val check_program_libraries : unit -> unit
diff --git a/vernac/retrieveObl.ml b/vernac/retrieveObl.ml
new file mode 100644
index 0000000000..c529972b8d
--- /dev/null
+++ b/vernac/retrieveObl.ml
@@ -0,0 +1,296 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+
+(**
+   - Get types of existentials ;
+   - Flatten dependency tree (prefix order) ;
+   - Replace existentials by de Bruijn indices in term, applied to the right arguments ;
+   - Apply term prefixed by quantification on "existentials".
+*)
+
+let check_evars env evm =
+  Evar.Map.iter
+    (fun key evi ->
+      if Evd.is_obligation_evar evm key then ()
+      else
+        let loc, k = Evd.evar_source key evm in
+        Pretype_errors.error_unsolvable_implicit ?loc env evm key None)
+    (Evd.undefined_map evm)
+
+type obligation_info =
+  ( Names.Id.t
+  * Constr.types
+  * Evar_kinds.t Loc.located
+  * (bool * Evar_kinds.obligation_definition_status)
+  * Int.Set.t
+  * unit Proofview.tactic option )
+  array
+
+type oblinfo =
+  { ev_name : int * Id.t
+  ; ev_hyps : EConstr.named_context
+  ; ev_status : bool * Evar_kinds.obligation_definition_status
+  ; ev_chop : int option
+  ; ev_src : Evar_kinds.t Loc.located
+  ; ev_typ : Constr.types
+  ; ev_tac : unit Proofview.tactic option
+  ; ev_deps : Int.Set.t }
+
+(** Substitute evar references in t using de Bruijn indices,
+  where n binders were passed through. *)
+
+let succfix (depth, fixrels) = (succ depth, List.map succ fixrels)
+
+let subst_evar_constr evm evs n idf t =
+  let seen = ref Int.Set.empty in
+  let transparent = ref Id.Set.empty in
+  let evar_info id = CList.assoc_f Evar.equal id evs in
+  let rec substrec (depth, fixrels) c =
+    match EConstr.kind evm c with
+    | Constr.Evar (k, args) ->
+      let {ev_name = id, idstr; ev_hyps = hyps; ev_chop = chop} =
+        try evar_info k
+        with Not_found ->
+          CErrors.anomaly ~label:"eterm"
+            Pp.(
+              str "existential variable "
+              ++ int (Evar.repr k)
+              ++ str " not found.")
+      in
+      seen := Int.Set.add id !seen;
+      (* Evar arguments are created in inverse order,
+         and we must not apply to defined ones (i.e. LetIn's)
+      *)
+      let args =
+        let n = match chop with None -> 0 | Some c -> c in
+        let l, r = CList.chop n (List.rev (Array.to_list args)) in
+        List.rev r
+      in
+      let args =
+        let rec aux hyps args acc =
+          let open Context.Named.Declaration in
+          match (hyps, args) with
+          | LocalAssum _ :: tlh, c :: tla ->
+            aux tlh tla (substrec (depth, fixrels) c :: acc)
+          | LocalDef _ :: tlh, _ :: tla -> aux tlh tla acc
+          | [], [] -> acc
+          | _, _ -> acc
+          (*failwith "subst_evars: invalid argument"*)
+        in
+        aux hyps args []
+      in
+      if
+        List.exists
+          (fun x ->
+            match EConstr.kind evm x with
+            | Constr.Rel n -> Int.List.mem n fixrels
+            | _ -> false)
+          args
+      then transparent := Id.Set.add idstr !transparent;
+      EConstr.mkApp (idf idstr, Array.of_list args)
+    | Constr.Fix _ ->
+      EConstr.map_with_binders evm succfix substrec (depth, 1 :: fixrels) c
+    | _ -> EConstr.map_with_binders evm succfix substrec (depth, fixrels) c
+  in
+  let t' = substrec (0, []) t in
+  (EConstr.to_constr evm t', !seen, !transparent)
+
+(** Substitute variable references in t using de Bruijn indices,
+  where n binders were passed through. *)
+let subst_vars acc n t =
+  let var_index id = Util.List.index Id.equal id acc in
+  let rec substrec depth c =
+    match Constr.kind c with
+    | Constr.Var v -> (
+      try Constr.mkRel (depth + var_index v) with Not_found -> c )
+    | _ -> Constr.map_with_binders succ substrec depth c
+  in
+  substrec 0 t
+
+(** Rewrite type of an evar ([ H1 : t1, ... Hn : tn |- concl ])
+    to a product : forall H1 : t1, ..., forall Hn : tn, concl.
+    Changes evars and hypothesis references to variable references.
+*)
+let etype_of_evar evm evs hyps concl =
+  let open Context.Named.Declaration in
+  let rec aux acc n = function
+    | decl :: tl -> (
+      let t', s, trans =
+        subst_evar_constr evm evs n EConstr.mkVar
+          (Context.Named.Declaration.get_type decl)
+      in
+      let t'' = subst_vars acc 0 t' in
+      let rest, s', trans' =
+        aux (Context.Named.Declaration.get_id decl :: acc) (succ n) tl
+      in
+      let s' = Int.Set.union s s' in
+      let trans' = Id.Set.union trans trans' in
+      match decl with
+      | LocalDef (id, c, _) ->
+        let c', s'', trans'' = subst_evar_constr evm evs n EConstr.mkVar c in
+        let c' = subst_vars acc 0 c' in
+        ( Term.mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest
+        , Int.Set.union s'' s'
+        , Id.Set.union trans'' trans' )
+      | LocalAssum (id, _) ->
+        (Term.mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans') )
+    | [] ->
+      let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in
+      (subst_vars acc 0 t', s, trans)
+  in
+  aux [] 0 (List.rev hyps)
+
+let trunc_named_context n ctx =
+  let len = List.length ctx in
+  CList.firstn (len - n) ctx
+
+let rec chop_product n t =
+  let pop t = Vars.lift (-1) t in
+  if Int.equal n 0 then Some t
+  else
+    match Constr.kind t with
+    | Constr.Prod (_, _, b) ->
+      if Vars.noccurn 1 b then chop_product (pred n) (pop b) else None
+    | _ -> None
+
+let evar_dependencies evm oev =
+  let one_step deps =
+    Evar.Set.fold
+      (fun ev s ->
+        let evi = Evd.find evm ev in
+        let deps' = Evd.evars_of_filtered_evar_info evm evi in
+        if Evar.Set.mem oev deps' then
+          invalid_arg
+            ( "Ill-formed evar map: cycle detected for evar "
+            ^ Pp.string_of_ppcmds @@ Evar.print oev )
+        else Evar.Set.union deps' s)
+      deps deps
+  in
+  let rec aux deps =
+    let deps' = one_step deps in
+    if Evar.Set.equal deps deps' then deps else aux deps'
+  in
+  aux (Evar.Set.singleton oev)
+
+let move_after ((id, ev, deps) as obl) l =
+  let rec aux restdeps = function
+    | ((id', _, _) as obl') :: tl ->
+      let restdeps' = Evar.Set.remove id' restdeps in
+      if Evar.Set.is_empty restdeps' then obl' :: obl :: tl
+      else obl' :: aux restdeps' tl
+    | [] -> [obl]
+  in
+  aux (Evar.Set.remove id deps) l
+
+let sort_dependencies evl =
+  let rec aux l found list =
+    match l with
+    | ((id, ev, deps) as obl) :: tl ->
+      let found' = Evar.Set.union found (Evar.Set.singleton id) in
+      if Evar.Set.subset deps found' then aux tl found' (obl :: list)
+      else aux (move_after obl tl) found list
+    | [] -> List.rev list
+  in
+  aux evl Evar.Set.empty []
+
+let retrieve_obligations env name evm fs ?status t ty =
+  (* 'Serialize' the evars *)
+  let nc = Environ.named_context env in
+  let nc_len = Context.Named.length nc in
+  let evm = Evarutil.nf_evar_map_undefined evm in
+  let evl = Evarutil.non_instantiated evm in
+  let evl = Evar.Map.bindings evl in
+  let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in
+  let sevl = sort_dependencies evl in
+  let evl = List.map (fun (id, ev, _) -> (id, ev)) sevl in
+  let evn =
+    let i = ref (-1) in
+    List.rev_map
+      (fun (id, ev) ->
+        incr i;
+        ( id
+        , ( !i
+          , Id.of_string
+              (Id.to_string name ^ "_obligation_" ^ string_of_int (succ !i)) )
+        , ev ))
+      evl
+  in
+  let evts =
+    (* Remove existential variables in types and build the corresponding products *)
+    List.fold_right
+      (fun (id, (n, nstr), ev) l ->
+        let hyps = Evd.evar_filtered_context ev in
+        let hyps = trunc_named_context nc_len hyps in
+        let evtyp, deps, transp = etype_of_evar evm l hyps ev.Evd.evar_concl in
+        let evtyp, hyps, chop =
+          match chop_product fs evtyp with
+          | Some t -> (t, trunc_named_context fs hyps, fs)
+          | None -> (evtyp, hyps, 0)
+        in
+        let loc, k = Evd.evar_source id evm in
+        let status =
+          match k with
+          | Evar_kinds.QuestionMark {Evar_kinds.qm_obligation = o} -> o
+          | _ -> (
+            match status with
+            | Some o -> o
+            | None ->
+              Evar_kinds.Define (not (Program.get_proofs_transparency ())) )
+        in
+        let force_status, status, chop =
+          match status with
+          | Evar_kinds.Define true as stat ->
+            if not (Int.equal chop fs) then (true, Evar_kinds.Define false, None)
+            else (false, stat, Some chop)
+          | s -> (false, s, None)
+        in
+        let info =
+          { ev_name = (n, nstr)
+          ; ev_hyps = hyps
+          ; ev_status = (force_status, status)
+          ; ev_chop = chop
+          ; ev_src = (loc, k)
+          ; ev_typ = evtyp
+          ; ev_deps = deps
+          ; ev_tac = None }
+        in
+        (id, info) :: l)
+      evn []
+  in
+  let t', _, transparent =
+    (* Substitute evar refs in the term by variables *)
+    subst_evar_constr evm evts 0 EConstr.mkVar t
+  in
+  let ty, _, _ = subst_evar_constr evm evts 0 EConstr.mkVar ty in
+  let evars =
+    List.map
+      (fun (ev, info) ->
+        let { ev_name = _, name
+            ; ev_status = force_status, status
+            ; ev_src = src
+            ; ev_typ = typ
+            ; ev_deps = deps
+            ; ev_tac = tac } =
+          info
+        in
+        let force_status, status =
+          match status with
+          | Evar_kinds.Define true when Id.Set.mem name transparent ->
+            (true, Evar_kinds.Define false)
+          | _ -> (force_status, status)
+        in
+        (name, typ, src, (force_status, status), deps, tac))
+      evts
+  in
+  let evnames = List.map (fun (ev, info) -> (ev, snd info.ev_name)) evts in
+  let evmap f c = Util.pi1 (subst_evar_constr evm evts 0 f c) in
+  (Array.of_list (List.rev evars), (evnames, evmap), t', ty)
diff --git a/vernac/retrieveObl.mli b/vernac/retrieveObl.mli
new file mode 100644
index 0000000000..c9c45bd889
--- /dev/null
+++ b/vernac/retrieveObl.mli
@@ -0,0 +1,46 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+val check_evars : Environ.env -> Evd.evar_map -> unit
+
+type obligation_info =
+  ( Names.Id.t
+  * Constr.types
+  * Evar_kinds.t Loc.located
+  * (bool * Evar_kinds.obligation_definition_status)
+  * Int.Set.t
+  * unit Proofview.tactic option )
+  array
+(** ident, type, location of the original evar, (opaque or
+   transparent, expand or define), dependencies as indexes into the
+   array, tactic to solve it *)
+
+val retrieve_obligations :
+     Environ.env
+  -> Names.Id.t
+  -> Evd.evar_map
+  -> int
+  -> ?status:Evar_kinds.obligation_definition_status
+  -> EConstr.t
+  -> EConstr.types
+  -> obligation_info
+     * ( (Evar.t * Names.Id.t) list
+       * ((Names.Id.t -> EConstr.t) -> EConstr.t -> Constr.t) )
+     * Constr.t
+     * Constr.t
+(** [retrieve_obligations env id sigma fs ?status body type] returns
+   [obls, (evnames, evmap), nbody, ntype] a list of obligations built
+   from evars in [body, type].
+
+    [fs] is the number of function prototypes to try to clear from
+   evars contexts. [evnames, evmap) is the list of names /
+   substitution functions used to program with holes. This is not used
+   in Coq, but in the equations plugin; [evnames] is actually
+   redundant with the information contained in [obls] *)
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 6e398d87ca..5a2bdb43d4 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -14,6 +14,7 @@ Proof_using
 Egramcoq
 Metasyntax
 DeclareUniv
+RetrieveObl
 DeclareDef
 DeclareObl
 Canonical
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 963b5f2084..4806c6bb9c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -527,8 +527,10 @@ let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in
   Some (DeclareDef.Hook.(make (fun { S.dref } -> Canonical.declare_canonical_structure dref)))
 | _ -> None
 
+let default_thm_id = Id.of_string "Unnamed_thm"
+
 let fresh_name_for_anonymous_theorem () =
-  Namegen.next_global_ident_away Lemmas.default_thm_id Id.Set.empty
+  Namegen.next_global_ident_away default_thm_id Id.Set.empty
 
 let vernac_definition_name lid local =
   let lid =
@@ -565,7 +567,9 @@ let vernac_definition ~atts (discharge, kind) (lid, pl) bl red_option c typ_opt
       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:name.v
+  let do_definition =
+    ComDefinition.(if program_mode then do_definition_program else do_definition) in
+  do_definition ~name:name.v
     ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook
 
 (* NB: pstate argument to use combinators easily *)