Merge PR #9645: [proof] Remove terminator type, unifying regular and obligation ones.

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

30 files changed, 1111 insertions, 871 deletions

diff --git a/dev/ci/user-overlays/09645-ejgallego-proof+sayonara_baby.sh b/dev/ci/user-overlays/09645-ejgallego-proof+sayonara_baby.sh
new file mode 100644
index 0000000000..3029f3019c
--- /dev/null
+++ b/dev/ci/user-overlays/09645-ejgallego-proof+sayonara_baby.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "9645" ] || [ "$CI_BRANCH" = "proof+sayonara_baby" ]; then
+
+    equations_CI_REF=proof+sayonara_baby
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    mtac2_CI_REF=proof+sayonara_baby
+    mtac2_CI_GITURL=https://github.com/ejgallego/Mtac2
+
+    paramcoq_CI_REF=proof+sayonara_baby
+    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+fi
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index a884ab3cf6..72ca5dc8c4 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -8,16 +8,9 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Constr
 open Context
 open Context.Named.Declaration
 
-let map_const_entry_body (f:constr->constr) (x: Evd.side_effects Entries.const_entry_body)
-    : Evd.side_effects Entries.const_entry_body =
-  Future.chain x begin fun ((b,ctx),fx) ->
-    (f b , ctx) , fx
-  end
-
 (** [start_deriving f suchthat lemma] starts a proof of [suchthat]
     (which can contain references to [f]) in the context extended by
     [f:=?x]. When the proof ends, [f] is defined as the value of [?x]
@@ -36,71 +29,18 @@ let start_deriving f suchthat name : Lemmas.t =
   (* create the initial goals for the proof: |- Type ; |- ?1 ; f:=?2 |- suchthat *)
   let goals =
     let open Proofview in
-        TCons ( env , sigma , f_type_type , (fun sigma f_type ->
+    TCons ( env , sigma , f_type_type , (fun sigma f_type ->
         TCons ( env , sigma , f_type , (fun sigma ef ->
-        let f_type = EConstr.Unsafe.to_constr f_type in
-        let ef = EConstr.Unsafe.to_constr ef in
-        let env' = Environ.push_named (LocalDef (annotR f, ef, f_type)) env in
-        let sigma, suchthat = Constrintern.interp_type_evars ~program_mode:false env' sigma suchthat in
-        TCons ( env' , sigma , suchthat , (fun sigma _ ->
-        TNil sigma))))))
-    in
-
-    (* The terminator handles the registering of constants when the proof is closed. *)
-    let terminator com =
-      (* Extracts the relevant information from the proof. [Admitted]
-         and [Save] result in user errors. [opaque] is [true] if the
-         proof was concluded by [Qed], and [false] if [Defined]. [f_def]
-         and [lemma_def] correspond to the proof of [f] and of
-         [suchthat], respectively. *)
-      let (opaque,f_def,lemma_def) =
-        match com with
-        | Lemmas.Admitted _ -> CErrors.user_err Pp.(str "Admitted isn't supported in Derive.")
-        | Lemmas.Proved (_,Some _,_) ->
-            CErrors.user_err Pp.(str "Cannot save a proof of Derive with an explicit name.")
-        | Lemmas.Proved (opaque, None, obj) ->
-            match Proof_global.(obj.entries) with
-            | [_;f_def;lemma_def] ->
-                opaque <> Proof_global.Transparent , f_def , lemma_def
-            | _ -> assert false
-      in
-      (* The opacity of [f_def] is adjusted to be [false], as it
-         must. Then [f] is declared in the global environment. *)
-      let f_def = { f_def with Entries.const_entry_opaque = false } in
-      let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in
-      let f_kn = Declare.declare_constant f f_def in
-      let f_kn_term = mkConst f_kn in
-      (* In the type and body of the proof of [suchthat] there can be
-         references to the variable [f]. It needs to be replaced by
-         references to the constant [f] declared above. This substitution
-         performs this precise action. *)
-      let substf c = Vars.replace_vars [f,f_kn_term] c in
-      (* Extracts the type of the proof of [suchthat]. *)
-      let lemma_pretype =
-        match Entries.(lemma_def.const_entry_type) with
-        | Some t -> t
-        | None -> assert false (* Proof_global always sets type here. *)
-      in
-      (* The references of [f] are subsituted appropriately. *)
-      let lemma_type = substf lemma_pretype in
-      (* The same is done in the body of the proof. *)
-      let lemma_body =
-        map_const_entry_body substf Entries.(lemma_def.const_entry_body)
-      in
-      let lemma_def = let open Entries in { lemma_def with
-        const_entry_body = lemma_body ;
-        const_entry_type = Some lemma_type ;
-        const_entry_opaque = opaque ; }
-      in
-      let lemma_def =
-        Entries.DefinitionEntry lemma_def ,
-        Decl_kinds.(IsProof Proposition)
-      in
-      ignore (Declare.declare_constant name lemma_def)
+            let f_type = EConstr.Unsafe.to_constr f_type in
+            let ef = EConstr.Unsafe.to_constr ef in
+            let env' = Environ.push_named (LocalDef (annotR f, ef, f_type)) env in
+            let sigma, suchthat = Constrintern.interp_type_evars ~program_mode:false env' sigma suchthat in
+            TCons ( env' , sigma , suchthat , (fun sigma _ ->
+                TNil sigma))))))
   in
 
-  let terminator ?hook _ = Lemmas.Internal.make_terminator terminator in
-  let lemma = Lemmas.start_dependent_lemma name kind goals ~terminator in
+  let proof_ending = Lemmas.Proof_ending.(End_derive {f; name}) in
+  let lemma = Lemmas.start_dependent_lemma name kind goals ~proof_ending 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_types.ml b/plugins/funind/functional_principles_types.ml
index 2fe1d1ff40..48eac96ab3 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -307,7 +307,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
   in
   let sigma, _ = Typing.type_of ~refresh:true (Global.env ()) !evd (EConstr.of_constr new_principle_type) in
   evd := sigma;
-  let hook = Lemmas.mk_hook (hook new_principle_type) in
+  let hook = DeclareDef.Hook.make (hook new_principle_type) in
   let lemma =
     Lemmas.start_lemma
       new_princ_name
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 7683ce1757..732a0d818f 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -137,7 +137,7 @@ let save id const ?hook uctx (locality,_,kind) =
         let kn = declare_constant id ~local (DefinitionEntry const, k) in
         ConstRef kn
   in
-  Lemmas.call_hook ?hook ~fix_exn uctx [] locality r;
+  DeclareDef.Hook.call ?hook ~fix_exn uctx [] locality r;
   definition_message id
 
 let with_full_print f a =
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 4078c34331..8dd990775b 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -45,7 +45,7 @@ val jmeq_refl : unit -> EConstr.constr
 val save
   :  Id.t
   -> Evd.side_effects Entries.definition_entry
-  -> ?hook:Lemmas.declaration_hook
+  -> ?hook:DeclareDef.Hook.t
   -> UState.t
   -> Decl_kinds.goal_kind
   -> unit
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 1ee5407bcc..b049e3607c 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1371,7 +1371,7 @@ let open_new_goal ~lemma build_proof sigma using_lemmas ref_ goal_name (gls_type
   let lemma = Lemmas.start_lemma
     na
     Decl_kinds.(Global ImportDefaultBehavior, false (* FIXME *), Proof Lemma)
-    sigma gls_type ~hook:(Lemmas.mk_hook hook) in
+    sigma gls_type ~hook:(DeclareDef.Hook.make hook) in
   let lemma = if Indfun_common.is_strict_tcc  ()
   then
     fst @@ Lemmas.by (Proofview.V82.tactic (tclIDTAC)) lemma
@@ -1592,5 +1592,5 @@ let recursive_definition ~interactive_proof ~is_mes function_name rec_impls type
         term_id
         using_lemmas
         (List.length res_vars)
-        evd (Lemmas.mk_hook hook))
+        evd (DeclareDef.Hook.make hook))
     ()
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 1b8f4f5069..4c29d73038 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2006,7 +2006,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
       declare_projection n instance_id (ConstRef cst)
     | _ -> assert false
   in
-  let hook = Lemmas.mk_hook hook in
+  let hook = DeclareDef.Hook.make hook in
   Flags.silently
     (fun () ->
        let lemma = Lemmas.start_lemma ~hook instance_id kind (Evd.from_ctx uctx) (EConstr.of_constr instance) in
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index bddea41145..0b1a7fcc03 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -24,9 +24,6 @@ module NamedDecl = Context.Named.Declaration
 
 (*** Proof Global Environment ***)
 
-(* Extra info on proofs. *)
-type lemma_possible_guards = int list list
-
 type proof_object = {
   id : Names.Id.t;
   entries : Evd.side_effects Entries.definition_entry list;
@@ -264,14 +261,22 @@ let return_proof ?(allow_partial=false) ps =
   let evd = Proof.return ~pid proof in
   let eff = Evd.eval_side_effects evd in
   let evd = Evd.minimize_universes evd in
-  (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
-     side-effects... This may explain why one need to uniquize side-effects
-     thereafter... *)
   let proof_opt c =
     match EConstr.to_constr_opt evd c with
     | Some p -> p
     | None -> CErrors.user_err Pp.(str "Some unresolved existential variables remain")
   in
+  (* ppedrot: FIXME, this is surely wrong. There is no reason to duplicate
+     side-effects... This may explain why one need to uniquize side-effects
+     thereafter... *)
+  (* EJGA: actually side-effects de-duplication and this codepath is
+     unrelated. Duplicated side-effects arise from incorrect scheme
+     generation code, the main bulk of it was mostly fixed by #9836
+     but duplication can still happen because of rewriting schemes I
+     think; however the code below is mostly untested, the only
+     code-paths that generate several proof entries are derive and
+     equations and so far there is no code in the CI that will
+     actually call those and do a side-effect, TTBOMK *)
   let proofs =
     List.map (fun (c, _) -> (proof_opt c, eff)) initial_goals in
     proofs, Evd.evar_universe_context evd
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 162f02b654..15685bd9b6 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -31,8 +31,6 @@ val compact_the_proof : t -> t
     function which takes a [proof_object] together with a [proof_end]
     (i.e. an proof ending command) and registers the appropriate
     values. *)
-type lemma_possible_guards = int list list
-
 type proof_object = {
   id : Names.Id.t;
   entries : Evd.side_effects Entries.definition_entry list;
diff --git a/stm/stm.ml b/stm/stm.ml
index 8e28b8a0e9..89d95d0cc9 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -208,7 +208,7 @@ let mkTransCmd cast cids ceff cqueue =
 (* Parts of the system state that are morally part of the proof state *)
 let summary_pstate = Evarutil.meta_counter_summary_tag,
                      Evd.evar_counter_summary_tag,
-                     Obligations.program_tcc_summary_tag
+                     DeclareObl.program_tcc_summary_tag
 
 type cached_state =
   | EmptyState
@@ -884,7 +884,7 @@ end = struct (* {{{ *)
     Lemmas.Stack.t option *
     int *                                   (* Evarutil.meta_counter_summary_tag *)
     int *                                   (* Evd.evar_counter_summary_tag *)
-    Obligations.program_info Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
+    DeclareObl.program_info CEphemeron.key Names.Id.Map.t (* Obligations.program_tcc_summary_tag *)
 
   type partial_state =
     [ `Full of Vernacstate.t
@@ -1532,14 +1532,12 @@ end = struct (* {{{ *)
           (* Unfortunately close_future_proof and friends are not pure so we need
              to set the state manually here *)
           State.unfreeze st;
-          let pobject, _ =
+          let pobject, _info =
             PG_compat.close_future_proof ~opaque ~feedback_id:stop (Future.from_val ~fix_exn p) in
-          let terminator = (* The one sent by master is an InvalidKey *)
-            Lemmas.(standard_proof_terminator []) in
 
           let st = Vernacstate.freeze_interp_state ~marshallable:false in
           stm_vernac_interp stop
-            ~proof:(pobject, terminator) st
+            ~proof:(pobject, Lemmas.default_info) st
             { verbose = false; indentation = 0; strlen = 0;
               expr = CAst.make ?loc @@ VernacExpr ([], VernacEndProof (Proved (opaque,None))) }) in
         ignore(Future.join checked_proof);
@@ -1676,10 +1674,10 @@ end = struct (* {{{ *)
       let opaque = Proof_global.Opaque in
 
       (* The original terminator, a hook, has not been saved in the .vio*)
-      let pterm, _invalid_terminator =
+      let pterm, _info =
         PG_compat.close_proof ~opaque ~keep_body_ucst_separate:true (fun x -> x) in
 
-      let proof = pterm , Lemmas.standard_proof_terminator [] in
+      let proof = pterm, Lemmas.default_info 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 *)
@@ -3242,7 +3240,7 @@ let unreachable_state_hook = Hooks.unreachable_state_hook
 let document_add_hook = Hooks.document_add_hook
 let document_edit_hook = Hooks.document_edit_hook
 let sentence_exec_hook = Hooks.sentence_exec_hook
-let () = Hook.set Obligations.stm_get_fix_exn (fun () -> !State.fix_exn_ref)
+let () = Hook.set DeclareObl.stm_get_fix_exn (fun () -> !State.fix_exn_ref)
 
 type document = VCS.vcs
 let backup () = VCS.backup ()
diff --git a/tactics/abstract.mli b/tactics/abstract.mli
index 779e46cd49..c474a01d1c 100644
--- a/tactics/abstract.mli
+++ b/tactics/abstract.mli
@@ -20,3 +20,11 @@ val cache_term_by_tactic_then
   -> unit Proofview.tactic
 
 val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic
+
+(* Internal but used in a few places; should likely be made intro a
+   proper library function, or incorporated into the generic constant
+   save path *)
+val shrink_entry
+  :  ('a, 'b) Context.Named.Declaration.pt list
+  -> 'c Entries.definition_entry
+  -> 'c Entries.definition_entry * Constr.t list
diff --git a/vernac/class.ml b/vernac/class.ml
index d08e680934..420baf7966 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -366,7 +366,7 @@ let add_coercion_hook poly _uctx _trans local ref =
   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 = Lemmas.mk_hook (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 stre = match local with
@@ -377,4 +377,4 @@ let add_subclass_hook poly _uctx _trans local ref =
   let cl = class_of_global ref in
   try_add_new_coercion_subclass cl ~local:stre poly
 
-let add_subclass_hook poly = Lemmas.mk_hook (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 4c7f3474f7..d530d218d4 100644
--- a/vernac/class.mli
+++ b/vernac/class.mli
@@ -42,8 +42,8 @@ val try_add_new_coercion_with_source : GlobRef.t -> local:bool ->
 val try_add_new_identity_coercion : Id.t -> local:bool -> 
   Decl_kinds.polymorphic -> source:cl_typ -> target:cl_typ -> unit
 
-val add_coercion_hook : Decl_kinds.polymorphic -> Lemmas.declaration_hook
+val add_coercion_hook : Decl_kinds.polymorphic -> DeclareDef.Hook.t
 
-val add_subclass_hook : Decl_kinds.polymorphic -> Lemmas.declaration_hook
+val add_subclass_hook : Decl_kinds.polymorphic -> DeclareDef.Hook.t
 
 val class_of_global : GlobRef.t -> cl_typ
diff --git a/vernac/classes.ml b/vernac/classes.ml
index d837bd010f..442f139827 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -361,7 +361,7 @@ let declare_instance_program env sigma ~global ~poly id pri imps decl term termt
       in obls, Some constr, typ
     | None -> [||], None, termtype
   in
-  let hook = Lemmas.mk_hook hook 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)
@@ -376,7 +376,7 @@ let declare_instance_open sigma ?hook ~tac ~global ~poly id pri imps decl ids te
   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:(Lemmas.mk_hook
+      ~hook:(DeclareDef.Hook.make
                (fun _ _ _ -> instance_hook pri global imps ?hook)) in
   (* spiwack: I don't know what to do with the status here. *)
   let lemma =
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 72392c07fc..af09a83f02 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -18,7 +18,7 @@ open Constrexpr
 
 val do_definition
   : program_mode:bool
-  -> ?hook:Lemmas.declaration_hook
+  -> ?hook:DeclareDef.Hook.t
   -> Id.t
   -> definition_kind
   -> universe_decl_expr option
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 85ff4f9d72..b42e877d41 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -88,7 +88,8 @@ val declare_fixpoint :
   locality -> polymorphic ->
   recursive_preentry * UState.universe_decl * UState.t *
   (Constr.rel_context * Impargs.manual_implicits * int option) list ->
-  Proof_global.lemma_possible_guards -> decl_notation list -> unit
+  Lemmas.lemma_possible_guards -> decl_notation list ->
+  unit
 
 val declare_cofixpoint :
   locality -> polymorphic ->
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index 563758df25..23c98c97f9 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -229,7 +229,7 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation =
       in hook, recname, typ
   in
   (* XXX: Capturing sigma here... bad bad *)
-  let hook = Lemmas.mk_hook (hook sigma) in
+  let hook = DeclareDef.Hook.make (hook sigma) in
   Obligations.check_evars env sigma;
   let evars, _, evars_def, evars_typ =
     Obligations.eterm_obligations env recname sigma 0 def typ
@@ -248,7 +248,7 @@ let collect_evars_of_term evd c ty =
   evars (Evd.from_ctx (Evd.evar_universe_context evd))
 
 let do_program_recursive local poly fixkind fixl ntns =
-  let cofix = fixkind = Obligations.IsCoFixpoint in
+  let cofix = fixkind = DeclareObl.IsCoFixpoint in
   let (env, rec_sign, pl, evd), fix, info =
     interp_recursive ~cofix ~program_mode:true fixl ntns
   in
@@ -289,8 +289,8 @@ let do_program_recursive local poly fixkind fixl ntns =
   end in
   let ctx = Evd.evar_universe_context evd in
   let kind = match fixkind with
-  | Obligations.IsFixpoint _ -> (local, poly, Fixpoint)
-  | Obligations.IsCoFixpoint -> (local, poly, CoFixpoint)
+  | DeclareObl.IsFixpoint _ -> (local, poly, Fixpoint)
+  | DeclareObl.IsCoFixpoint -> (local, poly, CoFixpoint)
   in
   Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind
 
@@ -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 = Obligations.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in
+        let fixkind = DeclareObl.IsFixpoint (List.map (fun d -> d.fix_annot) fixl) in
           do_program_recursive local poly fixkind fixl ntns
 
     | _, _ ->
@@ -341,5 +341,5 @@ let do_fixpoint local poly l =
 
 let do_cofixpoint local poly l =
   let fixl,ntns = extract_cofixpoint_components l in
-  do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns;
+  do_program_recursive local poly DeclareObl.IsCoFixpoint fixl ntns;
   if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()
diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml
index 93cd67a9d3..42327d6bdd 100644
--- a/vernac/declareDef.ml
+++ b/vernac/declareDef.ml
@@ -14,6 +14,29 @@ open Entries
 open Globnames
 open Impargs
 
+(* 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
+      -> Names.GlobRef.t
+      -> unit
+  end
+
+  type t = S.t CEphemeron.key
+
+  let make hook = CEphemeron.create hook
+
+  let call ?hook ?fix_exn uctx trans l c =
+    try Option.iter (fun hook -> CEphemeron.get hook uctx trans l c) hook
+    with e when CErrors.noncritical e ->
+      let e = CErrors.push e in
+      let e = Option.cata (fun fix -> fix e) e fix_exn in
+      Util.iraise e
+end
+
+(* Locality stuff *)
 let declare_definition ident (local, p, k) ?hook_data ce pl imps =
   let fix_exn = Future.fix_exn_of ce.const_entry_body in
   let gr = match local with
@@ -32,7 +55,7 @@ let declare_definition ident (local, p, k) ?hook_data ce pl imps =
     match hook_data with
     | None -> ()
     | Some (hook, uctx, extra_defs) ->
-      Lemmas.call_hook ~fix_exn ~hook uctx extra_defs local gr
+      Hook.call ~fix_exn ~hook uctx extra_defs local gr
   end;
   gr
 
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli
index e9e051f732..6f9608f04a 100644
--- a/vernac/declareDef.mli
+++ b/vernac/declareDef.mli
@@ -11,10 +11,38 @@
 open Names
 open Decl_kinds
 
+(** Declaration hooks *)
+module Hook : sig
+  type t
+
+  (** Hooks allow users of the API to perform arbitrary actions at
+     proof/definition saving time. For example, to register a constant
+     as a Coercion, perform some cleanup, update the search database,
+     etc...  *)
+  module S : sig
+    (** [S.t] passes to the client: *)
+    type t
+      =  UState.t
+      (** [ustate]: universe constraints obtained when the term was closed *)
+      -> (Id.t * Constr.t) list
+      (** [(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 of the original declaration *)
+      -> GlobRef.t
+      (** [ref]: identifier of the origianl declaration *)
+      -> unit
+  end
+
+  val make : S.t -> t
+  val call : ?hook:t -> ?fix_exn:Future.fix_exn -> S.t
+end
+
 val declare_definition
   : Id.t
   -> definition_kind
-  -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
+  -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
   -> Evd.side_effects Entries.definition_entry
   -> UnivNames.universe_binders
   -> Impargs.manual_implicits
@@ -22,7 +50,7 @@ val declare_definition
 
 val declare_fix
   : ?opaque:bool
-  -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list)
+  -> ?hook_data:(Hook.t * UState.t * (Id.t * Constr.t) list)
   -> definition_kind
   -> UnivNames.universe_binders
   -> Entries.universes_entry
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
new file mode 100644
index 0000000000..30aa347692
--- /dev/null
+++ b/vernac/declareObl.ml
@@ -0,0 +1,562 @@
+(************************************************************************)
+(*         *   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 Util
+open Names
+open Environ
+open Context
+open Constr
+open Vars
+open Decl_kinds
+open Entries
+
+type 'a obligation_body = DefinedObl of 'a | TermObl of constr
+
+type obligation =
+  { obl_name : Id.t
+  ; obl_type : types
+  ; obl_location : Evar_kinds.t Loc.located
+  ; obl_body : pconstant obligation_body option
+  ; obl_status : bool * Evar_kinds.obligation_definition_status
+  ; obl_deps : Int.Set.t
+  ; obl_tac : unit Proofview.tactic option }
+
+type obligations = obligation array * int
+
+type notations =
+  (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
+
+type fixpoint_kind =
+  | IsFixpoint of lident option list
+  | IsCoFixpoint
+
+type program_info =
+  { prg_name : Id.t
+  ; prg_body : constr
+  ; prg_type : constr
+  ; prg_ctx : UState.t
+  ; prg_univdecl : UState.universe_decl
+  ; prg_obligations : obligations
+  ; prg_deps : Id.t list
+  ; prg_fixkind : fixpoint_kind option
+  ; prg_implicits : Impargs.manual_implicits
+  ; prg_notations : notations
+  ; prg_kind : definition_kind
+  ; prg_reduce : constr -> constr
+  ; prg_hook : DeclareDef.Hook.t option
+  ; prg_opaque : bool
+  ; prg_sign : named_context_val }
+
+(* Saving an obligation *)
+
+let get_shrink_obligations =
+  Goptions.declare_bool_option_and_ref ~depr:true (* remove in 8.8 *)
+    ~name:"Shrinking of Program obligations" ~key:["Shrink"; "Obligations"]
+    ~value:true
+
+(* XXX: Is this the right place for this? *)
+let it_mkLambda_or_LetIn_or_clean t ctx =
+  let open Context.Rel.Declaration in
+  let fold t decl =
+    if is_local_assum decl then Term.mkLambda_or_LetIn decl t
+    else if noccurn 1 t then subst1 mkProp t
+    else Term.mkLambda_or_LetIn decl t
+  in
+  Context.Rel.fold_inside fold ctx ~init:t
+
+(* XXX: Is this the right place for this? *)
+let decompose_lam_prod c ty =
+  let open Context.Rel.Declaration in
+  let rec aux ctx c ty =
+    match (Constr.kind c, Constr.kind ty) with
+    | LetIn (x, b, t, c), LetIn (x', b', t', ty)
+      when Constr.equal b b' && Constr.equal t t' ->
+      let ctx' = Context.Rel.add (LocalDef (x, b', t')) ctx in
+      aux ctx' c ty
+    | _, LetIn (x', b', t', ty) ->
+      let ctx' = Context.Rel.add (LocalDef (x', b', t')) ctx in
+      aux ctx' (lift 1 c) ty
+    | LetIn (x, b, t, c), _ ->
+      let ctx' = Context.Rel.add (LocalDef (x, b, t)) ctx in
+      aux ctx' c (lift 1 ty)
+    | Lambda (x, b, t), Prod (x', b', t')
+    (* By invariant, must be convertible *) ->
+      let ctx' = Context.Rel.add (LocalAssum (x, b')) ctx in
+      aux ctx' t t'
+    | Cast (c, _, _), _ -> aux ctx c ty
+    | _, _ -> (ctx, c, ty)
+  in
+  aux Context.Rel.empty c ty
+
+(* XXX: What's the relation of this with Abstract.shrink ? *)
+let shrink_body c ty =
+  let ctx, b, ty =
+    match ty with
+    | None ->
+      let ctx, b = Term.decompose_lam_assum c in
+      (ctx, b, None)
+    | Some ty ->
+      let ctx, b, ty = decompose_lam_prod c ty in
+      (ctx, b, Some ty)
+  in
+  let b', ty', n, args =
+    List.fold_left
+      (fun (b, ty, i, args) decl ->
+        if noccurn 1 b && Option.cata (noccurn 1) true ty then
+          (subst1 mkProp b, Option.map (subst1 mkProp) ty, succ i, args)
+        else
+          let open Context.Rel.Declaration in
+          let args = if is_local_assum decl then mkRel i :: args else args in
+          ( Term.mkLambda_or_LetIn decl b
+          , Option.map (Term.mkProd_or_LetIn decl) ty
+          , succ i
+          , args ) )
+      (b, ty, 1, []) ctx
+  in
+  (ctx, b', ty', Array.of_list args)
+
+let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
+
+let add_hint local prg cst =
+  Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst)
+
+(***********************************************************************)
+(* Saving an obligation                                                *)
+(***********************************************************************)
+
+(* true = hide obligations *)
+let get_hide_obligations =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~name:"Hidding of Program obligations"
+    ~key:["Hide"; "Obligations"]
+    ~value:false
+
+let declare_obligation prg obl body ty uctx =
+  let body = prg.prg_reduce body in
+  let ty = Option.map prg.prg_reduce ty in
+  match obl.obl_status with
+  | _, 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 ctx, body, ty, args =
+      if get_shrink_obligations () && not poly then shrink_body body ty
+      else ([], body, ty, [||])
+    in
+    let body =
+      ((body, Univ.ContextSet.empty), Evd.empty_side_effects)
+    in
+    let ce =
+      { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body
+      ; const_entry_secctx = None
+      ; const_entry_type = ty
+      ; const_entry_universes = uctx
+      ; const_entry_opaque = opaque
+      ; const_entry_inline_code = false
+      ; const_entry_feedback = None }
+    in
+    (* ppedrot: seems legit to have obligations as local *)
+    let constant =
+      Declare.declare_constant obl.obl_name ~local:ImportNeedQualified
+        (DefinitionEntry ce, IsProof Property)
+    in
+    if not opaque then
+      add_hint (Locality.make_section_locality None) prg constant;
+    Declare.definition_message obl.obl_name;
+    let body =
+      match uctx with
+      | Polymorphic_entry (_, uctx) ->
+        Some (DefinedObl (constant, Univ.UContext.instance uctx))
+      | Monomorphic_entry _ ->
+        Some
+          (TermObl
+             (it_mkLambda_or_LetIn_or_clean
+                (mkApp (mkConst constant, args))
+                ctx))
+    in
+    (true, {obl with obl_body = body})
+
+(* Updating the obligation meta-info on close *)
+
+let not_transp_msg =
+  Pp.(
+    str "Obligation should be transparent but was declared opaque."
+    ++ spc ()
+    ++ str "Use 'Defined' instead.")
+
+let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
+let err_not_transp () = pperror not_transp_msg
+
+module ProgMap = Id.Map
+
+let from_prg, program_tcc_summary_tag =
+  Summary.ref_tag ProgMap.empty ~name:"program-tcc-table"
+
+(* In all cases, the use of the map is read-only so we don't expose the ref *)
+let get_prg_info_map () = !from_prg
+
+let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
+
+let close sec =
+  if not (ProgMap.is_empty !from_prg) then
+    let keys = map_keys !from_prg in
+    CErrors.user_err ~hdr:"Program"
+      Pp.(
+        str "Unsolved obligations when closing "
+        ++ str sec ++ str ":" ++ spc ()
+        ++ prlist_with_sep spc (fun x -> Id.print x) keys
+        ++ ( str (if Int.equal (List.length keys) 1 then " has " else " have ")
+           ++ str "unsolved obligations" ))
+
+let input : program_info CEphemeron.key ProgMap.t -> Libobject.obj =
+  let open Libobject in
+  declare_object
+    { (default_object "Program state") with
+      cache_function = (fun (na, pi) -> from_prg := pi)
+    ; load_function = (fun _ (_, pi) -> from_prg := pi)
+    ; discharge_function =
+        (fun _ ->
+          close "section";
+          None )
+    ; classify_function =
+        (fun _ ->
+          close "module";
+          Dispose ) }
+
+let map_replace k v m =
+  ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m)
+
+let progmap_remove prg =
+  Lib.add_anonymous_leaf (input (ProgMap.remove prg.prg_name !from_prg))
+
+let progmap_add n prg =
+  Lib.add_anonymous_leaf (input (ProgMap.add n prg !from_prg))
+
+let progmap_replace prg' =
+  Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg))
+
+let obligations_solved prg = Int.equal (snd prg.prg_obligations) 0
+
+let obligations_message rem =
+  if rem > 0 then
+    if Int.equal rem 1 then
+      Flags.if_verbose Feedback.msg_info
+        Pp.(int rem ++ str " obligation remaining")
+    else
+      Flags.if_verbose Feedback.msg_info
+        Pp.(int rem ++ str " obligations remaining")
+  else
+    Flags.if_verbose Feedback.msg_info Pp.(str "No more obligations remaining")
+
+type progress = Remain of int | Dependent | Defined of GlobRef.t
+
+let get_obligation_body expand obl =
+  match obl.obl_body with
+  | None -> None
+  | Some c -> (
+    if expand && snd obl.obl_status == Evar_kinds.Expand then
+      match c with
+      | DefinedObl pc -> Some (constant_value_in (Global.env ()) pc)
+      | TermObl c -> Some c
+    else
+      match c with DefinedObl pc -> Some (mkConstU pc) | TermObl c -> Some c )
+
+let obl_substitution expand obls deps =
+  Int.Set.fold
+    (fun x acc ->
+      let xobl = obls.(x) in
+      match get_obligation_body expand xobl with
+      | None -> acc
+      | Some oblb -> (xobl.obl_name, (xobl.obl_type, oblb)) :: acc )
+    deps []
+
+let rec intset_to = function
+  | -1 -> Int.Set.empty
+  | n -> Int.Set.add n (intset_to (pred n))
+
+let obligation_substitution expand prg =
+  let obls, _ = prg.prg_obligations in
+  let ints = intset_to (pred (Array.length obls)) in
+  obl_substitution expand obls ints
+
+let hide_obligation () =
+  Coqlib.check_required_library ["Coq"; "Program"; "Tactics"];
+  UnivGen.constr_of_monomorphic_global
+    (Coqlib.lib_ref "program.tactics.obligation")
+
+(* XXX: Is this the right place? *)
+let rec prod_app t n =
+  match
+    Constr.kind
+      (EConstr.Unsafe.to_constr
+         (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t)))
+    (* FIXME *)
+  with
+  | Prod (_, _, b) -> subst1 n b
+  | LetIn (_, b, t, b') -> prod_app (subst1 b b') n
+  | _ ->
+    CErrors.user_err ~hdr:"prod_app"
+      Pp.(str "Needed a product, but didn't find one" ++ fnl ())
+
+(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
+let prod_applist t nL = List.fold_left prod_app t nL
+
+let replace_appvars subst =
+  let rec aux c =
+    let f, l = decompose_app c in
+    if isVar f then
+      try
+        let c' = List.map (Constr.map aux) l in
+        let t, b = Id.List.assoc (destVar f) subst in
+        mkApp
+          ( delayed_force hide_obligation
+          , [|prod_applist t c'; Term.applistc b c'|] )
+      with Not_found -> Constr.map aux c
+    else Constr.map aux c
+  in
+  Constr.map aux
+
+let subst_prog subst prg =
+  if get_hide_obligations () then
+    ( replace_appvars subst prg.prg_body
+    , replace_appvars subst (* Termops.refresh_universes *) prg.prg_type )
+  else
+    let subst' = List.map (fun (n, (_, b)) -> (n, b)) subst in
+    ( Vars.replace_vars subst' prg.prg_body
+    , Vars.replace_vars subst' (* Termops.refresh_universes *) prg.prg_type )
+
+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 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:(pi2 prg.prg_kind) 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
+    prg.prg_implicits ?hook_data
+
+let rec lam_index n t acc =
+  match Constr.kind t with
+  | Lambda ({binder_name=Name n'}, _, _) when Id.equal n n' -> acc
+  | Lambda (_, _, b) -> lam_index n b (succ acc)
+  | _ -> raise Not_found
+
+let compute_possible_guardness_evidences n fixbody fixtype =
+  match n with
+  | Some {CAst.loc; v = n} -> [lam_index n fixbody 0]
+  | None ->
+    (* If recursive argument was not given by user, we try all args.
+         An earlier approach was to look only for inductive arguments,
+         but doing it properly involves delta-reduction, and it finally
+         doesn't seem to worth the effort (except for huge mutual
+         fixpoints ?) *)
+    let m =
+      Termops.nb_prod Evd.empty (EConstr.of_constr fixtype)
+      (* FIXME *)
+    in
+    let ctx = fst (Term.decompose_prod_n_assum m fixtype) in
+    List.map_i (fun i _ -> i) 0 ctx
+
+let mk_proof c =
+  ((c, Univ.ContextSet.empty), Evd.empty_side_effects)
+
+let declare_mutual_definition l =
+  let len = List.length l in
+  let first = List.hd l in
+  let defobl x =
+    let oblsubst = obligation_substitution true x in
+    let subs, typ = subst_prog oblsubst x in
+    let env = Global.env () in
+    let sigma = Evd.from_ctx x.prg_ctx in
+    let r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) in
+    let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in
+    let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in
+    let term = EConstr.to_constr sigma term in
+    let typ = EConstr.to_constr sigma typ in
+    let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_implicits) in
+    let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in
+    def, oblsubst
+  in
+  let defs, obls =
+    List.fold_right (fun x (defs, obls) ->
+        let xdef, xobls = defobl x in
+        (xdef :: defs, xobls @ obls)) l ([], [])
+  in
+  (*   let fixdefs = List.map reduce_fix fixdefs in *)
+  let fixdefs, fixrs,fixtypes, fiximps = List.split4 defs in
+  let fixkind = Option.get first.prg_fixkind in
+  let arrrec, recvec = (Array.of_list fixtypes, Array.of_list fixdefs) in
+  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
+  let indexes, fixdecls =
+    match fixkind with
+    | IsFixpoint wfl ->
+      let possible_indexes =
+        List.map3 compute_possible_guardness_evidences wfl fixdefs fixtypes
+      in
+      let indexes =
+        Pretyping.search_guard (Global.env ()) possible_indexes fixdecls
+      in
+      ( Some indexes
+      , List.map_i (fun i _ -> mk_proof (mkFix ((indexes, i), fixdecls))) 0 l
+      )
+    | IsCoFixpoint ->
+      (None, List.map_i (fun i _ -> mk_proof (mkCoFix (i, fixdecls))) 0 l)
+  in
+  (* Declare the recursive definitions *)
+  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)
+      fixnames fixdecls fixtypes fiximps
+  in
+  (* Declare notations *)
+  List.iter
+    (Metasyntax.add_notation_interpretation (Global.env ()))
+    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;
+  List.iter progmap_remove l;
+  gr
+
+let update_obls prg obls rem =
+  let prg' = {prg with prg_obligations = (obls, rem)} in
+  progmap_replace prg';
+  obligations_message rem;
+  if rem > 0 then Remain rem
+  else
+    match prg'.prg_deps with
+    | [] ->
+      let kn = declare_definition prg' in
+      progmap_remove prg';
+      Defined kn
+    | l ->
+      let progs =
+        List.map
+          (fun x -> CEphemeron.get (ProgMap.find x !from_prg))
+          prg'.prg_deps
+      in
+      if List.for_all (fun x -> obligations_solved x) progs then
+        let kn = declare_mutual_definition progs in
+        Defined kn
+      else Dependent
+
+let dependencies obls n =
+  let res = ref Int.Set.empty in
+  Array.iteri
+    (fun i obl ->
+      if (not (Int.equal i n)) && Int.Set.mem n obl.obl_deps then
+        res := Int.Set.add i !res )
+    obls;
+  !res
+
+type obligation_qed_info =
+  { name : Id.t
+  ; num : int
+  ; auto : Id.t option -> Int.Set.t -> unit Proofview.tactic option -> progress
+  }
+
+let obligation_terminator opq entries uctx { name; num; auto } =
+  let open Proof_global in
+  match entries with
+  | [entry] ->
+    let env = Global.env () in
+    let ty = entry.Entries.const_entry_type in
+    let body, eff = Future.force entry.const_entry_body in
+    let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
+    let sigma = Evd.from_ctx uctx in
+    let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
+    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, rem = prg.prg_obligations in
+    let obl = obls.(num) in
+    let status =
+      match obl.obl_status, opq with
+      | (_, Evar_kinds.Expand), Opaque -> err_not_transp ()
+      | (true, _), Opaque -> err_not_transp ()
+      | (false, _), Opaque -> Evar_kinds.Define true
+      | (_, Evar_kinds.Define true), Transparent ->
+        Evar_kinds.Define false
+      | (_, status), Transparent -> status
+    in
+    let obl = { obl with obl_status = false, status } in
+    let ctx =
+      if pi2 prg.prg_kind then ctx
+      else UState.union prg.prg_ctx ctx
+    in
+    let uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) 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 *)
+        (* We merge the new universes and constraints of the
+           polymorphic obligation with the existing ones *)
+        UState.union prg.prg_ctx ctx
+      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 (Global.universes ())
+        else ctx
+    in
+    let prg = {prg with prg_ctx} in
+    begin try
+      ignore (update_obls prg obls (pred rem));
+      if pred rem > 0 then
+        let deps = dependencies obls num in
+        if not (Int.Set.is_empty deps) then
+          ignore (auto (Some name) deps None)
+    with e when CErrors.noncritical e ->
+      let e = CErrors.push e in
+      pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))
+    end
+  | _ ->
+    CErrors.anomaly
+      Pp.(
+        str
+          "[obligation_terminator] close_proof returned more than one proof \
+           term")
diff --git a/vernac/declareObl.mli b/vernac/declareObl.mli
new file mode 100644
index 0000000000..70a4601ac6
--- /dev/null
+++ b/vernac/declareObl.mli
@@ -0,0 +1,114 @@
+(************************************************************************)
+(*         *   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
+open Constr
+
+type 'a obligation_body = DefinedObl of 'a | TermObl of constr
+
+type obligation =
+  { obl_name : Id.t
+  ; obl_type : types
+  ; obl_location : Evar_kinds.t Loc.located
+  ; obl_body : pconstant obligation_body option
+  ; obl_status : bool * Evar_kinds.obligation_definition_status
+  ; obl_deps : Int.Set.t
+  ; obl_tac : unit Proofview.tactic option }
+
+type obligations = obligation array * int
+
+type notations =
+  (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
+
+type fixpoint_kind =
+  | IsFixpoint of lident option list
+  | IsCoFixpoint
+
+type program_info =
+  { prg_name : Id.t
+  ; prg_body : constr
+  ; prg_type : constr
+  ; prg_ctx : UState.t
+  ; prg_univdecl : UState.universe_decl
+  ; prg_obligations : obligations
+  ; prg_deps : Id.t list
+  ; prg_fixkind : fixpoint_kind option
+  ; prg_implicits : Impargs.manual_implicits
+  ; prg_notations : notations
+  ; prg_kind : Decl_kinds.definition_kind
+  ; prg_reduce : constr -> constr
+  ; prg_hook : DeclareDef.Hook.t option
+  ; prg_opaque : bool
+  ; prg_sign : Environ.named_context_val }
+
+val declare_obligation :
+     program_info
+  -> obligation
+  -> Constr.types
+  -> Constr.types option
+  -> Entries.universes_entry
+  -> bool * obligation
+(** [declare_obligation] Save an obligation *)
+
+module ProgMap : CMap.ExtS with type key = Id.t and module Set := Id.Set
+
+val declare_definition : program_info -> Names.GlobRef.t
+
+type progress =
+  (* Resolution status of a program *)
+  | Remain of int
+  (* n obligations remaining *)
+  | Dependent
+  (* Dependent on other definitions *)
+  | Defined of GlobRef.t
+  (* Defined as id *)
+
+type obligation_qed_info =
+  { name : Id.t
+  ; num : int
+  ; auto : Id.t option -> Int.Set.t -> unit Proofview.tactic option -> progress
+  }
+
+val obligation_terminator
+  :  Proof_global.opacity_flag
+  -> Evd.side_effects Entries.definition_entry list
+  -> UState.t
+  -> obligation_qed_info -> unit
+(** [obligation_terminator] part 2 of saving an obligation *)
+
+val update_obls :
+     program_info
+  -> obligation array
+  -> int
+  -> progress
+(** [update_obls prg obls n progress] What does this do? *)
+
+(** { 2 Util }  *)
+
+val get_prg_info_map : unit -> program_info CEphemeron.key ProgMap.t
+
+val program_tcc_summary_tag :
+  program_info CEphemeron.key Id.Map.t Summary.Dyn.tag
+
+val obl_substitution :
+     bool
+  -> obligation array
+  -> Int.Set.t
+  -> (ProgMap.key * (Constr.types * Constr.types)) list
+
+val dependencies : obligation array -> int -> Int.Set.t
+
+val err_not_transp : unit -> unit
+val progmap_add : ProgMap.key -> program_info CEphemeron.key -> unit
+
+(* This is a hack to make it possible for Obligations to craft a Qed
+ * behind the scenes.  The fix_exn the Stm attaches to the Future proof
+ * is not available here, so we provide a side channel to get it *)
+val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) Hook.t
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 5b829917cb..400e0dfa3e 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -33,55 +33,60 @@ open Impargs
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
 
-type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit
-type declaration_hook = hook_type
-
-let mk_hook hook = hook
-
-let call_hook ?hook ?fix_exn uctx trans l c =
-  try Option.iter (fun hook -> hook uctx trans l c) hook
-  with e when CErrors.noncritical e ->
-    let e = CErrors.push e in
-    let e = Option.cata (fun fix -> fix e) e fix_exn in
-    iraise e
-
 (* Support for terminators and proofs with an associated constant
    [that can be saved] *)
 
-type proof_ending =
-  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
-  | Proved of Proof_global.opacity_flag *
-              lident option *
-              Proof_global.proof_object
+type lemma_possible_guards = int list list
+
+module Proof_ending = struct
 
-type proof_terminator = (proof_ending -> unit) CEphemeron.key
+  type t =
+    | 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
 
 (* Proofs with a save constant function *)
 type t =
   { proof : Proof_global.t
-  ; terminator : proof_terminator
+  ; 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 *)
   }
 
-let pf_map f { proof; terminator} = { proof = f proof; terminator }
-let pf_fold f ps = f ps.proof
+let pf_map f pf = { pf with proof = f pf.proof }
+let pf_fold f pf = f pf.proof
 
 let set_endline_tactic t = pf_map (Proof_global.set_endline_tactic t)
 
 (* To be removed *)
 module Internal = struct
 
-let make_terminator f = CEphemeron.create f
-let apply_terminator f = CEphemeron.get f
-
 (** Gets the current terminator without checking that the proof has
     been completed. Useful for the likes of [Admitted]. *)
-let get_terminator ps = ps.terminator
+let get_info ps = ps.hook, ps.compute_guard, ps.proof_ending
 
 end
+(* Internal *)
 
-let by tac { proof; terminator } =
-  let proof, res = Pfedit.by tac proof in
-  { proof; terminator}, res
+let by tac pf =
+  let proof, res = Pfedit.by tac pf.proof in
+  { pf with proof }, res
+
+(************************************************************************)
+(* Creating a lemma-like constant                                       *)
+(************************************************************************)
 
 (* Support for mutually proved theorems *)
 
@@ -206,38 +211,6 @@ let look_for_possibly_mutual_statements sigma = function
     Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds)
   | [] -> anomaly (Pp.str "Empty list of theorems.")
 
-(* Saving a goal *)
-
-let save ?export_seff id const uctx do_guard (locality,poly,kind) hook universes =
-  let fix_exn = Future.fix_exn_of const.Entries.const_entry_body in
-  try
-    let const = adjust_guardness_conditions const do_guard in
-    let k = Kindops.logical_kind_of_goal_kind kind in
-    let should_suggest = const.const_entry_opaque && Option.is_empty const.const_entry_secctx in
-    let r = match locality with
-      | Discharge ->
-          let c = SectionLocalDef const in
-          let _ = declare_variable id (Lib.cwd(), c, k) in
-          let () = if should_suggest
-            then Proof_using.suggest_variable (Global.env ()) id
-          in
-          VarRef id
-      | Global local ->
-          let kn =
-           declare_constant ?export_seff id ~local (DefinitionEntry const, k) in
-          let () = if should_suggest
-            then Proof_using.suggest_constant (Global.env ()) kn
-          in
-          let gr = ConstRef kn in
-          Declare.declare_univ_binders gr (UState.universe_binders uctx);
-          gr
-    in
-    definition_message id;
-    call_hook ?hook universes [] locality r
-  with e when CErrors.noncritical e ->
-    let e = CErrors.push e in
-    iraise (fix_exn e)
-
 let default_thm_id = Id.of_string "Unnamed_thm"
 
 let check_name_freshness locality {CAst.loc;v=id} : unit =
@@ -294,49 +267,6 @@ let save_remaining_recthms env sigma (locality,p,kind) norm univs body opaq i (i
         let kn = declare_constant id ~local (DefinitionEntry const, k) in
         (ConstRef kn,imps)
 
-let check_anonymity id save_ident =
-  if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
-    user_err Pp.(str "This command can only be used for unnamed theorem.")
-
-(* Admitted *)
-let warn_let_as_axiom =
-  CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
-                   (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++
-                                spc () ++ strbrk "declared as a local axiom.")
-
-let admit ?hook ctx (id,k,e) pl () =
-  let local = match k with
-  | Global local, _, _ -> local
-  | Discharge, _, _ -> warn_let_as_axiom id; ImportNeedQualified
-  in
-  let kn = declare_constant id ~local (ParameterEntry e, IsAssumption Conjectural) in
-  let () = assumption_message id in
-  Declare.declare_univ_binders (ConstRef kn) pl;
-  call_hook ?hook ctx [] (Global local) (ConstRef kn)
-
-(* Starting a goal *)
-
-let standard_proof_terminator ?(hook : declaration_hook option) compute_guard =
-  let open Proof_global in
-  CEphemeron.create begin function
-  | Admitted (id,k,pe,ctx) ->
-    let () = admit ?hook ctx (id,k,pe) (UState.universe_binders ctx) () in
-    Feedback.feedback Feedback.AddedAxiom
-  | Proved (opaque,idopt, { id; entries=[const]; persistence; universes } ) ->
-    let is_opaque, export_seff = match opaque with
-      | Transparent -> false, true
-      | Opaque      -> true, false
-    in
-    assert (is_opaque == const.const_entry_opaque);
-    let id = match idopt with
-      | None -> id
-      | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in
-    let () = save ~export_seff id const universes compute_guard persistence hook universes in
-    ()
-  | Proved (opaque,idopt, _ ) ->
-    CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term")
-  end
-
 let initialize_named_context_for_proof () =
   let sign = Global.named_context () in
   List.fold_right
@@ -372,34 +302,25 @@ module Stack = struct
     let (pn, pns) = map Proof.(function pf -> (data (prj pf.proof)).name) pf in
     pn :: pns
 
-  let copy_terminators ~src ~tgt =
+  let copy_info ~src ~tgt =
     let (ps, psl), (ts,tsl) = src, tgt in
     assert(List.length psl = List.length tsl);
-    {ts with terminator = ps.terminator}, List.map2 (fun op p -> { p with terminator = op.terminator }) psl tsl
+    { ps with proof = ts.proof },
+    List.map2 (fun op p -> { op with proof = p.proof }) psl tsl
 
 end
 
-let start_lemma id ?pl kind sigma ?terminator ?sign ?(compute_guard=[]) ?hook c =
-  let terminator = match terminator with
-  | None -> standard_proof_terminator ?hook compute_guard
-  | Some terminator -> terminator ?hook compute_guard
-  in
-  let sign =
-    match sign with
-    | Some sign -> sign
-    | None -> initialize_named_context_for_proof ()
-  in
+(* 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 goals = [ Global.env_of_context sign , c ] in
   let proof = Proof_global.start_proof sigma id ?pl kind goals in
-  { proof ; terminator }
+  { proof ; hook; compute_guard; proof_ending = CEphemeron.create proof_ending }
 
-let start_dependent_lemma id ?pl kind ?terminator ?sign ?(compute_guard=[]) ?hook telescope =
-  let terminator = match terminator with
-  | None -> standard_proof_terminator ?hook compute_guard
-  | Some terminator -> terminator ?hook compute_guard
-  in
+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 ; terminator }
+  { proof; hook; compute_guard; proof_ending = CEphemeron.create proof_ending }
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
@@ -446,7 +367,8 @@ let start_lemma_with_initialization ?hook kind sigma decl recguard thms snl =
         let thms_data = (ref,imps)::other_thms_data in
         List.iter (fun (ref,imps) ->
 	  maybe_declare_manual_implicits false ref imps;
-          call_hook ?hook ctx [] strength ref) thms_data in
+          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
@@ -488,24 +410,42 @@ let start_lemma_com ~program_mode ?inference_hook ?hook kind thms =
   in
   start_lemma_with_initialization ?hook kind evd decl recguard thms snl
 
-(* Saving a proof *)
+(************************************************************************)
+(* Admitting a lemma-like constant                                      *)
+(************************************************************************)
+
+let check_anonymity id save_ident =
+  if not (String.equal (atompart_of_id id) (Id.to_string (default_thm_id))) then
+    user_err Pp.(str "This command can only be used for unnamed theorem.")
+
+(* Admitted *)
+let warn_let_as_axiom =
+  CWarnings.create ~name:"let-as-axiom" ~category:"vernacular"
+                   (fun id -> strbrk "Let definition" ++ spc () ++ Id.print id ++
+                                spc () ++ strbrk "declared as an axiom.")
 
-let keep_admitted_vars = ref true
+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
 
-let () =
-  let open Goptions in
-  declare_bool_option
-    { optdepr  = false;
-      optname  = "keep section variables in admitted proofs";
-      optkey   = ["Keep"; "Admitted"; "Variables"];
-      optread  = (fun () -> !keep_admitted_vars);
-      optwrite = (fun b -> keep_admitted_vars := b) }
+let get_keep_admitted_vars =
+  Goptions.declare_bool_option_and_ref
+    ~depr:false
+    ~name:"keep section variables in admitted proofs"
+    ~key:["Keep"; "Admitted"; "Variables"]
+    ~value:true
 
 let save_lemma_admitted ?proof ~(lemma : t) =
-  let pe =
     let open Proof_global in
     match proof with
-    | Some ({ id; entries; persistence = k; universes }, _) ->
+    | Some ({ id; entries; persistence = k; universes }, (hook, _, _)) ->
       if List.length entries <> 1 then
         user_err Pp.(str "Admitted does not support multiple statements");
       let { const_entry_secctx; const_entry_type } = List.hd entries in
@@ -513,8 +453,8 @@ let save_lemma_admitted ?proof ~(lemma : t) =
         user_err Pp.(str "Admitted requires an explicit statement");
       let typ = Option.get const_entry_type in
       let ctx = UState.univ_entry ~poly:(pi2 k) universes in
-      let sec_vars = if !keep_admitted_vars then const_entry_secctx else None in
-      Admitted(id, k, (sec_vars, (typ, ctx), None), universes)
+      let sec_vars = if get_keep_admitted_vars () then const_entry_secctx else None in
+      finish_admitted id k (sec_vars, (typ, ctx), None) universes hook
     | None ->
       let pftree = Proof_global.get_proof lemma.proof in
       let gk = Proof_global.get_persistence lemma.proof in
@@ -531,7 +471,7 @@ let save_lemma_admitted ?proof ~(lemma : t) =
       let pproofs, _univs =
         Proof_global.return_proof ~allow_partial:true lemma.proof in
       let sec_vars =
-        if not !keep_admitted_vars then None
+        if not (get_keep_admitted_vars ()) then None
         else match Proof_global.get_used_variables lemma.proof, pproofs with
           | Some _ as x, _ -> x
           | None, (pproof, _) :: _ ->
@@ -542,21 +482,152 @@ let save_lemma_admitted ?proof ~(lemma : t) =
           | _ -> None in
       let decl = Proof_global.get_universe_decl lemma.proof in
       let ctx = UState.check_univ_decl ~poly universes decl in
-      Admitted(name,gk,(sec_vars, (typ, ctx), None), universes)
+      finish_admitted name gk (sec_vars, (typ, ctx), None) universes lemma.hook
+
+(************************************************************************)
+(* 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 open Proof_global in
+  match po with
+  | { id; entries=[const]; persistence=locality,poly,kind; universes } ->
+    let is_opaque, export_seff = match opaque with
+      | Transparent -> false, true
+      | Opaque      -> true, false
+    in
+    assert (is_opaque == const.const_entry_opaque);
+    let id = match idopt with
+      | None -> id
+      | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in
+    let fix_exn = Future.fix_exn_of const.Entries.const_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.const_entry_opaque && Option.is_empty const.const_entry_secctx in
+      let r = match locality with
+        | Discharge ->
+          let c = SectionLocalDef const in
+          let _ = declare_variable id (Lib.cwd(), c, k) in
+          let () = if should_suggest
+            then Proof_using.suggest_variable (Global.env ()) id
+          in
+          VarRef id
+        | Global local ->
+          let kn =
+            declare_constant ~export_seff id ~local (DefinitionEntry const, k) in
+          let () = if should_suggest
+            then Proof_using.suggest_constant (Global.env ()) kn
+          in
+          let gr = ConstRef kn in
+          Declare.declare_univ_binders gr (UState.universe_binders universes);
+          gr
+      in
+      definition_message id;
+      DeclareDef.Hook.call ~fix_exn ?hook universes [] locality r
+    with e when CErrors.noncritical e ->
+      let e = CErrors.push e in
+      iraise (fix_exn e)
+    in ()
+  | _ ->
+    CErrors.anomaly Pp.(str "[standard_proof_terminator] close_proof returned more than one proof term")
+
+let finish_derived ~f ~name ~idopt ~opaque ~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 opaque, f_def, lemma_def =
+    match entries with
+    | [_;f_def;lemma_def] ->
+      opaque <> Proof_global.Transparent , f_def , lemma_def
+    | _ -> assert false
+  in
+  (* The opacity of [f_def] is adjusted to be [false], as it
+     must. Then [f] is declared in the global environment. *)
+  let f_def = { f_def with Entries.const_entry_opaque = false } in
+  let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in
+  let f_kn = Declare.declare_constant f f_def in
+  let f_kn_term = mkConst f_kn in
+  (* In the type and body of the proof of [suchthat] there can be
+     references to the variable [f]. It needs to be replaced by
+     references to the constant [f] declared above. This substitution
+     performs this precise action. *)
+  let substf c = Vars.replace_vars [f,f_kn_term] c in
+  (* Extracts the type of the proof of [suchthat]. *)
+  let lemma_pretype =
+    match Entries.(lemma_def.const_entry_type) with
+    | Some t -> t
+    | None -> assert false (* Proof_global always sets type here. *)
   in
-  CEphemeron.get lemma.terminator pe
+  (* The references of [f] are subsituted appropriately. *)
+  let lemma_type = substf lemma_pretype in
+  (* The same is done in the body of the proof. *)
+  let lemma_body = Future.chain Entries.(lemma_def.const_entry_body) (fun ((b,ctx),fx) -> (substf b, ctx), fx) in
+  let lemma_def = let open Entries in
+    { lemma_def with
+      const_entry_body = lemma_body ;
+      const_entry_type = Some lemma_type ;
+      const_entry_opaque = opaque ; }
+  in
+  let lemma_def =
+    Entries.DefinitionEntry lemma_def ,
+    Decl_kinds.(IsProof Proposition)
+  in
+  ignore (Declare.declare_constant name lemma_def)
+
+let finish_proved_equations opaque lid 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
+    | DefinitionBody d -> IsDefinition d
+    | Proof p -> IsProof p
+  in
+  let sigma, recobls =
+    CList.fold_left2_map (fun sigma (wit, (evar_env, ev, evi, local_context, type_)) entry ->
+        let id =
+          match Evd.evar_ident ev sigma0 with
+          | Some id -> id
+          | None -> let n = !obls in incr obls; add_suffix i ("_obligation_" ^ string_of_int n)
+        in
+        let entry, args = Abstract.shrink_entry local_context entry in
+        let cst = Declare.declare_constant id (Entries.DefinitionEntry entry, kind) in
+        let sigma, app = Evarutil.new_global sigma (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
+  in
+  hook recobls sigma
 
 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,terminator) =
+  let 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; terminator } = Option.get lemma in
-      Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, terminator
-    | Some proof -> proof
+      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)
+    | Some (proof, info) ->
+      proof, info
   in
-  CEphemeron.get terminator (Proved (opaque,idopt,proof_obj))
+  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
+  | Regular ->
+    finish_proved opaque idopt proof_obj hook compute_guard
+  | 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
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 0806d747cd..70c8b511a1 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -11,36 +11,9 @@
 open Names
 open Decl_kinds
 
-(* Declaration hooks *)
-type declaration_hook
-
-(* Hooks allow users of the API to perform arbitrary actions at
- * proof/definition saving time. For example, to register a constant
- * as a Coercion, perform some cleanup, update the search database,
- * etc...
- *
- * Here, we use an extended hook type suitable for obligations /
- * equations.
- *)
-(** [hook_type] passes to the client:
-    - [ustate]: universe constraints obtained when the term was closed
-    - [(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)
-    - [locality]: Locality of the original declaration
-    - [ref]: identifier of the origianl declaration
- *)
-type hook_type = UState.t -> (Id.t * Constr.t) list -> Decl_kinds.locality -> GlobRef.t -> unit
-
-val mk_hook : hook_type -> declaration_hook
-val call_hook
-  :  ?hook:declaration_hook
-  -> ?fix_exn:Future.fix_exn
-  -> hook_type
-
-(* Proofs that define a constant + terminators *)
+(* Proofs that define a constant *)
 type t
-type proof_terminator
+type lemma_possible_guards = int list list
 
 module Stack : sig
 
@@ -58,17 +31,12 @@ module Stack : sig
 
   val get_all_proof_names : t -> Names.Id.t list
 
-  val copy_terminators : src:t -> tgt:t -> t
-  (** Gets the current terminator without checking that the proof has
-      been completed. Useful for the likes of [Admitted]. *)
+  val copy_info : src:t -> tgt:t -> t
+  (** Gets the current info without checking that the proof has been
+     completed. Useful for the likes of [Admitted]. *)
 
 end
 
-val standard_proof_terminator
-  :  ?hook:declaration_hook
-  -> Proof_global.lemma_possible_guards
-  -> proof_terminator
-
 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
@@ -77,15 +45,30 @@ val by : unit Proofview.tactic -> t -> t * bool
 
 (* Start of high-level proofs with an associated constant *)
 
+module Proof_ending : sig
+
+  type t =
+    | 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
+
 val start_lemma
   :  Id.t
   -> ?pl:UState.universe_decl
   -> goal_kind
   -> Evd.evar_map
-  -> ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> proof_terminator)
+  -> ?proof_ending:Proof_ending.t
   -> ?sign:Environ.named_context_val
-  -> ?compute_guard:Proof_global.lemma_possible_guards
-  -> ?hook:declaration_hook
+  -> ?compute_guard:lemma_possible_guards
+  -> ?hook:DeclareDef.Hook.t
   -> EConstr.types
   -> t
 
@@ -93,23 +76,22 @@ val start_dependent_lemma
   :  Id.t
   -> ?pl:UState.universe_decl
   -> goal_kind
-  -> ?terminator:(?hook:declaration_hook -> Proof_global.lemma_possible_guards -> proof_terminator)
-  -> ?sign:Environ.named_context_val
-  -> ?compute_guard:Proof_global.lemma_possible_guards
-  -> ?hook:declaration_hook
+  -> ?proof_ending:Proof_ending.t
+  -> ?compute_guard:lemma_possible_guards
+  -> ?hook:DeclareDef.Hook.t
   -> Proofview.telescope
   -> t
 
 val start_lemma_com
   :  program_mode:bool
   -> ?inference_hook:Pretyping.inference_hook
-  -> ?hook:declaration_hook -> goal_kind -> Vernacexpr.proof_expr list
+  -> ?hook:DeclareDef.Hook.t -> goal_kind -> Vernacexpr.proof_expr list
   -> t
 
 val start_lemma_with_initialization
-  :  ?hook:declaration_hook
+  :  ?hook:DeclareDef.Hook.t
   -> goal_kind -> Evd.evar_map -> UState.universe_decl
-  -> (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option
+  -> (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
@@ -125,33 +107,24 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val
 
 (** {6 Saving proofs } *)
 
+type proof_info
+
+val default_info : proof_info
+
 val save_lemma_admitted
-  :  ?proof:(Proof_global.proof_object * proof_terminator)
+  :  ?proof:(Proof_global.proof_object * proof_info)
   -> lemma:t
   -> unit
 
 val save_lemma_proved
-  :  ?proof:(Proof_global.proof_object * proof_terminator)
+  :  ?proof:(Proof_global.proof_object * proof_info)
   -> ?lemma:t
   -> opaque:Proof_global.opacity_flag
   -> idopt:Names.lident option
   -> unit
 
-(* API to build a terminator, should go away *)
-type proof_ending =
-  | Admitted of Names.Id.t * Decl_kinds.goal_kind * Entries.parameter_entry * UState.t
-  | Proved of Proof_global.opacity_flag *
-              Names.lident option *
-              Proof_global.proof_object
-
-(** This stuff is internal and will be removed in the future.  *)
+(* To be removed *)
 module Internal : sig
-
   (** Only needed due to the Proof_global compatibility layer. *)
-  val get_terminator : t -> proof_terminator
-
-  (** Only needed by obligations, should be reified soon *)
-  val make_terminator : (proof_ending -> unit) -> proof_terminator
-  val apply_terminator : proof_terminator -> proof_ending -> unit
-
+  val get_info : t -> proof_info
 end
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 6ef2f80067..cd8d22ac9a 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -1,8 +1,16 @@
+(************************************************************************)
+(*         *   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 Printf
-open Libobject
 open Entries
 open Decl_kinds
-open Declare
 
 (**
    - Get types of existentials ;
@@ -13,7 +21,6 @@ open Declare
 
 open Term
 open Constr
-open Context
 open Vars
 open Names
 open Evd
@@ -23,7 +30,7 @@ open Util
 
 module NamedDecl = Context.Named.Declaration
 
-let get_fix_exn, stm_get_fix_exn = Hook.make ()
+open DeclareObl
 
 let succfix (depth, fixrels) =
   (succ depth, List.map succ fixrels)
@@ -163,16 +170,16 @@ let evar_dependencies evm oev =
       else aux deps'
   in aux (Evar.Set.singleton oev)
 
-let move_after (id, ev, deps as obl) l = 
+let move_after (id, ev, deps as obl) l =
   let rec aux restdeps = function
-    | (id', _, _) as obl' :: tl -> 
+    | (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
@@ -186,7 +193,7 @@ let sort_dependencies evl =
 
 open Environ
 
-let eterm_obligations env name evm fs ?status t ty = 
+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
@@ -253,10 +260,6 @@ let eterm_obligations env name evm fs ?status t ty =
   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 hide_obligation () =
-  Coqlib.check_required_library ["Coq";"Program";"Tactics"];
-  UnivGen.constr_of_monomorphic_global (Coqlib.lib_ref "program.tactics.obligation")
-
 let pperror cmd = CErrors.user_err ~hdr:"Program" cmd
 let error s = pperror (str s)
 
@@ -276,386 +279,27 @@ type obligation_info =
        (bool * Evar_kinds.obligation_definition_status)
        * Int.Set.t * unit Proofview.tactic option) array
 
-type 'a obligation_body = 
-  | DefinedObl of 'a
-  | TermObl of constr
-
-type obligation =
-  { obl_name : Id.t;
-    obl_type : types;
-    obl_location : Evar_kinds.t Loc.located;
-    obl_body : pconstant obligation_body option;
-    obl_status : bool * Evar_kinds.obligation_definition_status;
-    obl_deps : Int.Set.t;
-    obl_tac : unit Proofview.tactic option;
-  }
-
-type obligations = (obligation array * int)
-
-type fixpoint_kind =
-  | IsFixpoint of lident option list
-  | IsCoFixpoint
-
-type notations = (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
-
-type program_info_aux = {
-  prg_name: Id.t;
-  prg_body: constr;
-  prg_type: constr;
-  prg_ctx:  UState.t;
-  prg_univdecl: UState.universe_decl;
-  prg_obligations: obligations;
-  prg_deps : Id.t list;
-  prg_fixkind : fixpoint_kind option ;
-  prg_implicits : Impargs.manual_implicits;
-  prg_notations : notations ;
-  prg_kind : definition_kind;
-  prg_reduce : constr -> constr;
-  prg_hook : Lemmas.declaration_hook option;
-  prg_opaque : bool;
-  prg_sign: named_context_val;
-}
-
-type program_info = program_info_aux CEphemeron.key
-
-let get_info x =
-  try CEphemeron.get x
-  with CEphemeron.InvalidKey ->
-    CErrors.anomaly Pp.(str "Program obligation can't be accessed by a worker.")
-
 let assumption_message = Declare.assumption_message
 
 let default_tactic = ref (Proofview.tclUNIT ())
 
-(* true = hide obligations *)
-let get_hide_obligations =
-  Goptions.declare_bool_option_and_ref
-    ~depr:false
-    ~name:"Hiding of Program obligations"
-    ~key:["Hide";"Obligations"]
-    ~value:false
-
-
-let get_shrink_obligations =
-  Goptions.declare_bool_option_and_ref
-    ~depr:true (* remove in 8.8 *)
-    ~name:"Shrinking of Program obligations"
-    ~key:["Shrink";"Obligations"]
-    ~value:true
-
 let evar_of_obligation o = make_evar (Global.named_context_val ()) (EConstr.of_constr o.obl_type)
 
-let get_obligation_body expand obl =
-  match obl.obl_body with
-  | None -> None
-  | Some c ->
-     if expand && snd obl.obl_status == Evar_kinds.Expand then
-       match c with
-       | DefinedObl pc -> Some (constant_value_in (Global.env ()) pc)
-       | TermObl c -> Some c
-     else (match c with
-	   | DefinedObl pc -> Some (mkConstU pc)
-	   | TermObl c -> Some c)
-
-let obl_substitution expand obls deps =
-  Int.Set.fold
-    (fun x acc ->
-       let xobl = obls.(x) in
-       match get_obligation_body expand xobl with
-       | None -> acc
-       | Some oblb -> (xobl.obl_name, (xobl.obl_type, oblb)) :: acc)
-    deps []
-
 let subst_deps expand obls deps t =
   let osubst = obl_substitution expand obls deps in
     (Vars.replace_vars (List.map (fun (n, (_, b)) -> n, b) osubst) t)
 
-let rec prod_app t n =
-  match Constr.kind (EConstr.Unsafe.to_constr (Termops.strip_outer_cast Evd.empty (EConstr.of_constr t))) (* FIXME *) with
-    | Prod (_,_,b) -> subst1 n b
-    | LetIn (_, b, t, b') -> prod_app (subst1 b b') n
-    | _ ->
-	user_err ~hdr:"prod_app"
-	  (str"Needed a product, but didn't find one" ++ fnl ())
-
-
-(* prod_appvect T [| a1 ; ... ; an |] -> (T a1 ... an) *)
-let prod_applist t nL = List.fold_left prod_app t nL
-
-let replace_appvars subst =
-  let rec aux c = 
-    let f, l = decompose_app c in
-      if isVar f then
-	try
-	  let c' = List.map (Constr.map aux) l in
-	  let (t, b) = Id.List.assoc (destVar f) subst in
-	    mkApp (delayed_force hide_obligation, 
-		   [| prod_applist t c'; applistc b c' |])
-	with Not_found -> Constr.map aux c
-      else Constr.map aux c
-  in Constr.map aux
-
 let subst_deps_obl obls obl =
   let t' = subst_deps true obls obl.obl_deps obl.obl_type in
     { obl with obl_type = t' }
 
-module ProgMap = Id.Map
-
-let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m)
-
-let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
-
-let from_prg, program_tcc_summary_tag =
-  Summary.ref_tag ProgMap.empty ~name:"program-tcc-table"
-
-let close sec =
-  if not (ProgMap.is_empty !from_prg) then
-    let keys = map_keys !from_prg in
-      user_err ~hdr:"Program" 
-	(str "Unsolved obligations when closing " ++ str sec ++ str":" ++ spc () ++
-	   prlist_with_sep spc (fun x -> Id.print x) keys ++
-	   (str (if Int.equal (List.length keys) 1 then " has " else " have ") ++
-	      str "unsolved obligations"))
-
-let input : program_info ProgMap.t -> obj =
-  declare_object
-    { (default_object "Program state") with
-      cache_function = (fun (na, pi) -> from_prg := pi);
-      load_function = (fun _ (_, pi) -> from_prg := pi);
-      discharge_function = (fun _ -> close "section"; None);
-      classify_function = (fun _ -> close "module"; Dispose) }
-    
 open Evd
 
-let progmap_remove prg =
-  Lib.add_anonymous_leaf (input (ProgMap.remove prg.prg_name !from_prg))
-  
-let progmap_add n prg =
-  Lib.add_anonymous_leaf (input (ProgMap.add n prg !from_prg))
-
-let progmap_replace prg' = 
-  Lib.add_anonymous_leaf (input (map_replace prg'.prg_name prg' !from_prg))
-
-let rec intset_to = function
-    -1 -> Int.Set.empty
-  | n -> Int.Set.add n (intset_to (pred n))
-
-let subst_prog subst prg =
-  if get_hide_obligations () then
-    (replace_appvars subst prg.prg_body,
-     replace_appvars subst ((* Termops.refresh_universes *) prg.prg_type))
-  else
-    let subst' = List.map (fun (n, (_, b)) -> n, b) subst in
-    (Vars.replace_vars subst' prg.prg_body,
-     Vars.replace_vars subst' ((* Termops.refresh_universes *) prg.prg_type))
-
-let obligation_substitution expand prg =
-  let obls, _ = prg.prg_obligations in
-  let ints = intset_to (pred (Array.length obls)) in
-  obl_substitution expand obls ints
-
-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 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:(pi2 prg.prg_kind) uctx prg.prg_univdecl in
-  let ce = 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 prg.prg_implicits ?hook_data
-
-let rec lam_index n t acc =
-  match Constr.kind t with
-    | Lambda ({binder_name=Name n'}, _, _) when Id.equal n n' ->
-      acc
-    | Lambda (_, _, b) ->
-	lam_index n b (succ acc)
-    | _ -> raise Not_found
-
-let compute_possible_guardness_evidences n fixbody fixtype =
-  match n with
-  | Some { CAst.loc; v = n } -> [lam_index n fixbody 0]
-  | None ->
-      (* If recursive argument was not given by user, we try all args.
-	 An earlier approach was to look only for inductive arguments,
-	 but doing it properly involves delta-reduction, and it finally
-         doesn't seem to worth the effort (except for huge mutual
-	 fixpoints ?) *)
-      let m = Termops.nb_prod Evd.empty (EConstr.of_constr fixtype) (* FIXME *) in
-      let ctx = fst (decompose_prod_n_assum m fixtype) in
-	List.map_i (fun i _ -> i) 0 ctx
-
-let mk_proof c = ((c, Univ.ContextSet.empty), Evd.empty_side_effects)
-
-let declare_mutual_definition l =
-  let len = List.length l in
-  let first = List.hd l in
-  let defobl x =
-    let oblsubst = obligation_substitution true x in
-    let subs, typ = subst_prog oblsubst x in
-    let env = Global.env () in
-    let sigma = Evd.from_ctx x.prg_ctx in
-    let r = Retyping.relevance_of_type env sigma (EConstr.of_constr typ) in
-    let term = snd (Reductionops.splay_lam_n env sigma len (EConstr.of_constr subs)) in
-    let typ = snd (Reductionops.splay_prod_n env sigma len (EConstr.of_constr typ)) in
-    let term = EConstr.to_constr sigma term in
-    let typ = EConstr.to_constr sigma typ in
-    let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_implicits) in
-    let oblsubst = List.map (fun (id, (_, c)) -> id, c) oblsubst in
-    def, oblsubst
-  in
-  let defs, obls =
-    List.fold_right (fun x (defs, obls) ->
-        let xdef, xobls = defobl x in
-        (xdef :: defs, xobls @ obls)) l ([], [])
-  in
-(*   let fixdefs = List.map reduce_fix fixdefs in *)
-  let fixdefs, fixrs, fixtypes, fiximps = List.split4 defs in
-  let fixkind = Option.get first.prg_fixkind in
-  let arrrec, recvec = Array.of_list fixtypes, Array.of_list fixdefs in
-  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
-  let indexes, fixdecls =
-    match fixkind with
-      | IsFixpoint wfl ->
-	  let possible_indexes =
-	    List.map3 compute_possible_guardness_evidences
-              wfl fixdefs fixtypes in
-	  let indexes = 
-              Pretyping.search_guard (Global.env())
-              possible_indexes fixdecls in
-          Some indexes, 
-          List.map_i (fun i _ ->
-            mk_proof (mkFix ((indexes,i),fixdecls))) 0 l
-      | IsCoFixpoint ->
-          None,
-          List.map_i (fun i _ ->
-            mk_proof (mkCoFix (i,fixdecls))) 0 l
-  in
-  (* Declare the recursive definitions *)
-  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)
-    fixnames fixdecls fixtypes fiximps in
-    (* Declare notations *)
-    List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations;
-    Declare.recursive_message (fixkind != IsCoFixpoint) indexes fixnames;
-    let gr = List.hd kns in
-    Lemmas.call_hook ?hook:first.prg_hook ~fix_exn first.prg_ctx obls local gr;
-    List.iter progmap_remove l; gr
-
-let decompose_lam_prod c ty =
-  let open Context.Rel.Declaration in
-  let rec aux ctx c ty =
-    match Constr.kind c, Constr.kind ty with
-    | LetIn (x, b, t, c), LetIn (x', b', t', ty)
-	 when Constr.equal b b' && Constr.equal t t' ->
-       let ctx' = Context.Rel.add (LocalDef (x,b',t')) ctx in
-       aux ctx' c ty
-    | _, LetIn (x', b', t', ty) ->
-       let ctx' = Context.Rel.add (LocalDef (x',b',t')) ctx in
-       aux ctx' (lift 1 c) ty
-    | LetIn (x, b, t, c), _ ->
-       let ctx' = Context.Rel.add (LocalDef (x,b,t)) ctx in
-       aux ctx' c (lift 1 ty)
-    | Lambda (x, b, t), Prod (x', b', t')
-       (* By invariant, must be convertible *) ->
-       let ctx' = Context.Rel.add (LocalAssum (x,b')) ctx in
-       aux ctx' t t'
-    | Cast (c, _, _), _ -> aux ctx c ty
-    | _, _ -> ctx, c, ty
-  in aux Context.Rel.empty c ty
-
-let shrink_body c ty =
-  let ctx, b, ty =
-    match ty with
-    | None ->
-       let ctx, b = decompose_lam_assum c in
-       ctx, b, None
-    | Some ty ->
-       let ctx, b, ty = decompose_lam_prod c ty in
-       ctx, b, Some ty
-  in
-  let b', ty', n, args =
-    List.fold_left (fun (b, ty, i, args) decl ->
-        if noccurn 1 b && Option.cata (noccurn 1) true ty then
-	  subst1 mkProp b, Option.map (subst1 mkProp) ty, succ i, args
-	else
-          let open Context.Rel.Declaration in
-	  let args = if is_local_assum decl then mkRel i :: args else args in
-          mkLambda_or_LetIn decl b, Option.map (mkProd_or_LetIn decl) ty,
-	  succ i, args)
-     (b, ty, 1, []) ctx
-  in ctx, b', ty', Array.of_list args
-
 let unfold_entry cst = Hints.HintsUnfoldEntry [EvalConstRef cst]
 
 let add_hint local prg cst =
   Hints.add_hints ~local [Id.to_string prg.prg_name] (unfold_entry cst)
 
-let it_mkLambda_or_LetIn_or_clean t ctx =
-  let open Context.Rel.Declaration in
-  let fold t decl =
-    if is_local_assum decl then mkLambda_or_LetIn decl t
-    else
-      if noccurn 1 t then subst1 mkProp t
-      else mkLambda_or_LetIn decl t
-  in
-  Context.Rel.fold_inside fold ctx ~init:t
-
-let declare_obligation prg obl body ty uctx =
-  let body = prg.prg_reduce body in
-  let ty = Option.map prg.prg_reduce ty in
-  match obl.obl_status with
-  | _, 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 ctx, body, ty, args =
-	if get_shrink_obligations () && not poly then
-	  shrink_body body ty else [], body, ty, [||]
-      in
-      let body = ((body,Univ.ContextSet.empty), Evd.empty_side_effects) in
-      let ce =
-        { const_entry_body = Future.from_val ~fix_exn:(fun x -> x) body;
-          const_entry_secctx = None;
-	  const_entry_type = ty;
-          const_entry_universes = uctx;
-	  const_entry_opaque = opaque;
-          const_entry_inline_code = false;
-          const_entry_feedback = None;
-      } in
-      (* ppedrot: seems legit to have obligations as local *)
-      let constant = Declare.declare_constant obl.obl_name ~local:ImportNeedQualified
-	(DefinitionEntry ce,IsProof Property)
-      in
-      if not opaque then add_hint (Locality.make_section_locality None) prg constant;
-      definition_message obl.obl_name;
-      let body = match uctx with
-        | Polymorphic_entry (_, uctx) ->
-          Some (DefinedObl (constant, Univ.UContext.instance uctx))
-        | Monomorphic_entry _ ->
-          Some (TermObl (it_mkLambda_or_LetIn_or_clean (mkApp (mkConst constant, args)) ctx))
-      in
-      true, { obl with obl_body = body }
-
 let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind
                    notations obls impls kind reduce =
   let obls', b =
@@ -671,27 +315,27 @@ let init_prog_info ?(opaque = false) ?hook sign n udecl b t ctx deps fixkind
     | Some b ->
 	Array.mapi
 	  (fun i (n, t, l, o, d, tac) ->
-            { obl_name = n ; obl_body = None; 
+            { obl_name = n ; obl_body = None;
 	      obl_location = l; obl_type = t; obl_status = o;
 	      obl_deps = d; obl_tac = tac })
 	  obls, b
   in
   let ctx = UState.make_flexible_nonalgebraic ctx in
-    { prg_name = n ; prg_body = b; prg_type = reduce t; 
+    { 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_implicits = impls; prg_kind = kind; prg_reduce = reduce;
       prg_hook = hook; prg_opaque = opaque;
       prg_sign = sign }
 
 let map_cardinal m =
   let i = ref 0 in
   ProgMap.iter (fun _ v ->
-		if snd (CEphemeron.get v).prg_obligations > 0 then incr i) m;
+      if snd (CEphemeron.get v).prg_obligations > 0 then incr i) m;
   !i
 
-exception Found of program_info
+exception Found of program_info CEphemeron.key
 
 let map_first m =
   try
@@ -702,28 +346,28 @@ let map_first m =
   with Found x -> x
 
 let get_prog name =
-  let prg_infos = !from_prg in
+  let prg_infos = get_prg_info_map () in
     match name with
 	Some n ->
-	  (try get_info (ProgMap.find n prg_infos)
+          (try CEphemeron.get (ProgMap.find n prg_infos)
 	   with Not_found -> raise (NoObligations (Some n)))
       | None ->
 	  (let n = map_cardinal prg_infos in
 	     match n with
 		 0 -> raise (NoObligations None)
-	       | 1 -> get_info (map_first prg_infos)
+               | 1 -> CEphemeron.get (map_first prg_infos)
 	       | _ ->
                 let progs = Id.Set.elements (ProgMap.domain prg_infos) in
                 let prog = List.hd progs in
                 let progs = prlist_with_sep pr_comma Id.print progs in
-                user_err 
+                user_err
                   (str "More than one program with unsolved obligations: " ++ progs
                   ++ str "; use the \"of\" clause to specify, as in \"Obligation 1 of " ++ Id.print prog ++ str "\""))
 
 let get_any_prog () =
-  let prg_infos = !from_prg in
+  let prg_infos = get_prg_info_map () in
   let n = map_cardinal prg_infos in
-  if n > 0 then get_info (map_first prg_infos)
+  if n > 0 then CEphemeron.get (map_first prg_infos)
   else raise (NoObligations None)
 
 let get_prog_err n =
@@ -732,42 +376,8 @@ let get_prog_err n =
 let get_any_prog_err () =
   try get_any_prog () with NoObligations id -> pperror (explain_no_obligations id)
 
-let obligations_solved prg = Int.equal (snd prg.prg_obligations) 0
-
 let all_programs () =
-  ProgMap.fold (fun k p l -> p :: l) !from_prg []
-
-type progress =
-    | Remain of int
-    | Dependent
-    | Defined of GlobRef.t
-
-let obligations_message rem =
-  if rem > 0 then
-    if Int.equal rem 1 then
-      Flags.if_verbose Feedback.msg_info (int rem ++ str " obligation remaining")
-    else
-      Flags.if_verbose Feedback.msg_info (int rem ++ str " obligations remaining")
-  else
-    Flags.if_verbose Feedback.msg_info (str "No more obligations remaining")
-
-let update_obls prg obls rem =
-  let prg' = { prg with prg_obligations = (obls, rem) } in
-    progmap_replace prg';
-    obligations_message rem;
-    if rem > 0 then Remain rem
-    else (
-      match prg'.prg_deps with
-      | [] ->
-          let kn = declare_definition prg' in
-            progmap_remove prg';
-	    Defined kn
-      | l ->
-	  let progs = List.map (fun x -> get_info (ProgMap.find x !from_prg)) prg'.prg_deps in
-	    if List.for_all (fun x -> obligations_solved x) progs then
-	      let kn = declare_mutual_definition progs in
-                Defined kn
-            else Dependent)
+  ProgMap.fold (fun k p l -> p :: l) (get_prg_info_map ()) []
 
 let is_defined obls x = not (Option.is_empty obls.(x).obl_body)
 
@@ -778,14 +388,6 @@ let deps_remaining obls deps =
       else x :: acc)
     deps []
 
-let dependencies obls n =
-  let res = ref Int.Set.empty in
-    Array.iteri
-      (fun i obl ->
-	if not (Int.equal i n) && Int.Set.mem n obl.obl_deps then
-	  res := Int.Set.add i !res)
-      obls;
-    !res
 
 let goal_kind poly =
   Decl_kinds.(Global ImportNeedQualified, poly, DefinitionBody Definition)
@@ -798,12 +400,6 @@ let kind_of_obligation poly o =
   | Evar_kinds.Define false | Evar_kinds.Expand -> goal_kind poly
   | _ -> goal_proof_kind poly
 
-let not_transp_msg =
-  str "Obligation should be transparent but was declared opaque." ++ spc () ++
-    str"Use 'Defined' instead."
-
-let err_not_transp () = pperror not_transp_msg
-
 let rec string_of_list sep f = function
     [] -> ""
   | x :: [] -> f x
@@ -839,81 +435,12 @@ let solve_by_tac ?loc name evi t poly ctx =
     warn_solve_errored ?loc err;
     None
 
-let obligation_terminator ?hook name num guard auto pf =
-  let open Proof_global in
-  let open Lemmas in
-  let term = standard_proof_terminator ?hook guard in
-  match pf with
-  | Admitted _ -> Internal.apply_terminator term pf
-  | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin
-    let env = Global.env () in
-    let ty = entry.Entries.const_entry_type in
-    let body, eff = Future.force entry.const_entry_body in
-    let (body, cstr) = Safe_typing.inline_private_constants env (body, eff.Evd.seff_private) in
-    let sigma = Evd.from_ctx uctx in
-    let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in
-    Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body);
-    (* Declare the obligation ourselves and drop the hook *)
-    let prg = get_info (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, rem = prg.prg_obligations in
-    let obl = obls.(num) in
-    let status =
-      match obl.obl_status, opq with
-      | (_, Evar_kinds.Expand), Opaque -> err_not_transp ()
-      | (true, _), Opaque -> err_not_transp ()
-      | (false, _), Opaque -> Evar_kinds.Define true
-      | (_, Evar_kinds.Define true), Transparent ->
-        Evar_kinds.Define false
-      | (_, status), Transparent -> status
-    in
-    let obl = { obl with obl_status = false, status } in
-    let ctx =
-      if pi2 prg.prg_kind then ctx
-      else UState.union prg.prg_ctx ctx
-    in
-    let uctx = UState.univ_entry ~poly:(pi2 prg.prg_kind) 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 *)
-        (* We merge the new universes and constraints of the
-           polymorphic obligation with the existing ones *)
-        UState.union prg.prg_ctx ctx
-      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 (Global.universes ())
-        else ctx
-    in
-    let prg = { prg with prg_ctx } in
-    try
-      ignore (update_obls prg obls (pred rem));
-      if pred rem > 0 then
-        begin
-          let deps = dependencies obls num in
-          if not (Int.Set.is_empty deps) then
-            ignore (auto (Some name) None deps)
-        end
-    with e when CErrors.noncritical e ->
-      let e = CErrors.push e in
-      pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e))
-  end
-  | Proved (_, _, _ ) ->
-    CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term")
-
 let obligation_hook prg obl num auto ctx' _ _ gr =
   let obls, rem = prg.prg_obligations in
   let cst = match gr with GlobRef.ConstRef cst -> cst | _ -> assert false in
   let transparent = evaluable_constant cst (Global.env ()) in
   let () = match obl.obl_status with
-      (true, Evar_kinds.Expand) 
+      (true, Evar_kinds.Expand)
     | (true, Evar_kinds.Define true) ->
        if not transparent then err_not_transp ()
     | _ -> ()
@@ -944,7 +471,7 @@ let obligation_hook prg obl num auto ctx' _ _ gr =
   if pred rem > 0 then begin
     let deps = dependencies obls num in
     if not (Int.Set.is_empty deps) then
-      ignore (auto (Some prg.prg_name) None deps)
+      ignore (auto (Some prg.prg_name) deps None)
   end
 
 let rec solve_obligation prg num tac =
@@ -963,12 +490,10 @@ let rec solve_obligation prg num tac =
   let kind = kind_of_obligation (pi2 prg.prg_kind) (snd obl.obl_status) in
   let evd = Evd.from_ctx prg.prg_ctx in
   let evd = Evd.update_sigma_env evd (Global.env ()) in
-  let auto n tac oblset = auto_solve_obligations n ~oblset tac in
-  let terminator ?hook guard =
-    Lemmas.Internal.make_terminator
-      (obligation_terminator prg.prg_name num guard ?hook auto) in
-  let hook = Lemmas.mk_hook (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) ~terminator ~hook 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 lemma = fst @@ Lemmas.by !default_tactic lemma in
   let lemma = Option.cata (fun tac -> Lemmas.set_endline_tactic tac lemma) lemma tac in
   lemma
@@ -1049,7 +574,7 @@ and solve_obligations n tac =
     solve_prg_obligations prg tac
 
 and solve_all_obligations tac =
-  ProgMap.iter (fun k v -> ignore(solve_prg_obligations (get_info v) tac)) !from_prg
+  ProgMap.iter (fun k v -> ignore(solve_prg_obligations (CEphemeron.get v) tac)) (get_prg_info_map ())
 
 and try_solve_obligation n prg tac =
   let prg = get_prog prg in
@@ -1091,9 +616,9 @@ let show_obligations ?(msg=true) n =
   let progs = match n with
     | None -> all_programs ()
     | Some n ->
-	try [ProgMap.find n !from_prg]
+        try [ProgMap.find n (get_prg_info_map ())]
 	with Not_found -> raise (NoObligations (Some n))
-  in List.iter (fun x -> show_obligations_of_prg ~msg (get_info x)) progs
+  in List.iter (fun x -> show_obligations_of_prg ~msg (CEphemeron.get x)) progs
 
 let show_term n =
   let prg = get_prog_err n in
@@ -1113,8 +638,8 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
   let obls,_ = prg.prg_obligations in
   if Int.equal (Array.length obls) 0 then (
     Flags.if_verbose Feedback.msg_info (info ++ str ".");
-    let cst = declare_definition prg in
-      Defined cst)
+    let cst = DeclareObl.declare_definition prg in
+    Defined cst)
   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
@@ -1140,8 +665,8 @@ let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
 	else
 	  let res = auto_solve_obligations (Some x) tactic in
 	    match res with
-	    | Defined _ -> 
-		(* If one definition is turned into a constant, 
+            | Defined _ ->
+                (* If one definition is turned into a constant,
 		   the whole block is defined. *) true
 	    | _ -> false)
 	false deps
@@ -1150,7 +675,7 @@ let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
 let admit_prog prg =
   let obls, rem = prg.prg_obligations in
   let obls = Array.copy obls in
-    Array.iteri 
+    Array.iteri
       (fun i x ->
         match x.obl_body with
         | None ->
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 8264a8071f..a0010a5026 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -13,11 +13,6 @@ open Constr
 open Evd
 open Names
 
-(* This is a hack to make it possible for Obligations to craft a Qed
- * behind the scenes.  The fix_exn the Stm attaches to the Future proof
- * is not available here, so we provide a side channel to get it *)
-val stm_get_fix_exn : (unit -> Exninfo.iexn -> Exninfo.iexn) Hook.t
-
 val check_evars : env -> evar_map -> unit
 
 val evar_dependencies : evar_map -> Evar.t -> Evar.Set.t
@@ -45,11 +40,6 @@ type obligation_info =
     (* ident, type, location, (opaque or transparent, expand or define),
        dependencies, tactic to solve it *)
 
-type progress = (* Resolution status of a program *)
-  | Remain of int  (* n obligations remaining *)
-  | Dependent (* Dependent on other definitions *)
-  | Defined of GlobRef.t (* Defined as id *)
-
 val default_tactic : unit Proofview.tactic ref
 
 val add_definition
@@ -61,17 +51,10 @@ val add_definition
   -> ?kind:Decl_kinds.definition_kind
   -> ?tactic:unit Proofview.tactic
   -> ?reduce:(constr -> constr)
-  -> ?hook:Lemmas.declaration_hook
+  -> ?hook:DeclareDef.Hook.t
   -> ?opaque:bool
   -> obligation_info
-  -> progress
-
-type notations =
-    (lstring * Constrexpr.constr_expr * Notation_term.scope_name option) list
-
-type fixpoint_kind =
-  | IsFixpoint of lident option list
-  | IsCoFixpoint
+  -> DeclareObl.progress
 
 val add_mutual_definitions :
   (Names.Id.t * constr * types * Impargs.manual_implicits * obligation_info) list ->
@@ -80,9 +63,9 @@ val add_mutual_definitions :
   ?tactic:unit Proofview.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   ?reduce:(constr -> constr) ->
-  ?hook:Lemmas.declaration_hook -> ?opaque:bool ->
-  notations ->
-  fixpoint_kind -> unit
+  ?hook:DeclareDef.Hook.t -> ?opaque:bool ->
+  DeclareObl.notations ->
+  DeclareObl.fixpoint_kind -> unit
 
 val obligation
   :  int * Names.Id.t option * Constrexpr.constr_expr option
@@ -94,7 +77,8 @@ val next_obligation
   -> Genarg.glob_generic_argument option
   -> Lemmas.t
 
-val solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> progress
+val solve_obligations : Names.Id.t option -> unit Proofview.tactic option
+  -> DeclareObl.progress
 (* Number of remaining obligations to be solved for this program *)
 
 val solve_all_obligations : unit Proofview.tactic option -> unit
@@ -114,6 +98,3 @@ exception NoObligations of Names.Id.t option
 val explain_no_obligations : Names.Id.t option -> Pp.t
 
 val check_program_libraries : unit -> unit
-
-type program_info
-val program_tcc_summary_tag : program_info Id.Map.t Summary.Dyn.tag
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 57c56a58f9..d28eeb341d 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -11,15 +11,16 @@ Egramml
 Vernacextend
 Ppvernac
 Proof_using
-Lemmas
-Canonical
-Class
 Egramcoq
 Metasyntax
+DeclareDef
+DeclareObl
+Canonical
+Lemmas
+Class
 Auto_ind_decl
 Search
 Indschemes
-DeclareDef
 Obligations
 ComDefinition
 Classes
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ac47a6a8f3..222f727f8e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -588,7 +588,7 @@ let vernac_definition_hook p = function
 | Coercion ->
   Some (Class.add_coercion_hook p)
 | CanonicalStructure ->
-  Some (Lemmas.mk_hook (fun _ _ _ -> Canonical.declare_canonical_structure))
+  Some (DeclareDef.Hook.make (fun _ _ _ -> Canonical.declare_canonical_structure))
 | SubClass ->
   Some (Class.add_subclass_hook p)
 | _ -> None
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 52da8b8de5..e46212ca1c 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_terminator) ->
+  ?proof:(Proof_global.proof_object * Lemmas.proof_info) ->
   st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t
 
 (** Prepare a "match" template for a given inductive type.
diff --git a/vernac/vernacstate.ml b/vernac/vernacstate.ml
index 43d705de5c..2bc20a747d 100644
--- a/vernac/vernacstate.ml
+++ b/vernac/vernacstate.ml
@@ -131,18 +131,18 @@ module Proof_global = struct
       s_lemmas := Some stack;
       res
 
-  type closed_proof = Proof_global.proof_object * Lemmas.proof_terminator
+  type closed_proof = Proof_global.proof_object * Lemmas.proof_info
 
 
   let return_proof ?allow_partial () = cc (return_proof ?allow_partial)
 
   let close_future_proof ~opaque ~feedback_id pf =
     cc_lemma (fun pt -> pf_fold (fun st -> close_future_proof ~opaque ~feedback_id st pf) pt,
-                        Internal.get_terminator pt)
+                        Internal.get_info pt)
 
   let close_proof ~opaque ~keep_body_ucst_separate f =
     cc_lemma (fun pt -> pf_fold ((close_proof ~opaque ~keep_body_ucst_separate f)) pt,
-                        Internal.get_terminator pt)
+                        Internal.get_info pt)
 
   let discard_all () = s_lemmas := None
   let update_global_env () = dd (update_global_env)
@@ -158,6 +158,6 @@ module Proof_global = struct
     | None, None -> None
     | Some _ , None -> None
     | None, Some x -> Some x
-    | Some src, Some tgt -> Some (Stack.copy_terminators ~src ~tgt)
+    | Some src, Some tgt -> Some (Stack.copy_info ~src ~tgt)
 
 end
diff --git a/vernac/vernacstate.mli b/vernac/vernacstate.mli
index bf908204ac..7e4d5d0315 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_terminator
+  type closed_proof = Proof_global.proof_object * Lemmas.proof_info
 
   val close_future_proof :
     opaque:Proof_global.opacity_flag ->