[proof] Remove terminator type, unifying regular and obligation ones.

We radically redesign how proof closing information is stored. Instead
of a user-defined closure, we now reify control into a single data
structure containing the needed information.

In this scheme, the `Lemmas` module can get extra information with
obligation info when opening the proof, and will correspondingly call
the right closing function based on this.

This is the start of what could be a much bigger unification of all
the proof save paths.

7 files changed, 165 insertions, 189 deletions

diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 0f0bec0129..0447b79dcd 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 = 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/vernac/declareObl.ml b/vernac/declareObl.ml
index b269f69ece..71215d2a3e 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -486,13 +486,16 @@ let dependencies obls n =
     obls;
   !res
 
-let obligation_terminator name num auto pf =
+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
-  let open Lemmas in
-  let term = Lemmas.standard_proof_terminator in
-  match pf with
-  | Admitted _ -> Internal.apply_terminator term pf
-  | Proved (opq, id, { entries=[entry]; universes=uctx }, hook, compute_guard ) -> begin
+  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
@@ -539,18 +542,20 @@ let obligation_terminator name num auto pf =
         if defined then UState.make (Global.universes ())
         else ctx
     in
-    let prg = { prg with prg_ctx } in
-    try
+    let prg = {prg with prg_ctx} in
+    begin 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
+        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
-  | Proved (_, _, _,_,_) ->
-    CErrors.anomaly Pp.(str "[obligation_terminator] close_proof returned more than one proof term")
+    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
index 5d02639245..70a4601ac6 100644
--- a/vernac/declareObl.mli
+++ b/vernac/declareObl.mli
@@ -61,14 +61,6 @@ module ProgMap : CMap.ExtS with type key = Id.t and module Set := Id.Set
 
 val declare_definition : program_info -> Names.GlobRef.t
 
-val obligation_terminator :
-     Id.t
-  -> int
-  -> (ProgMap.key option -> 'a option -> Int.Set.t -> 'b)
-  -> Lemmas.proof_ending
-  -> unit
-(** [obligation_terminator] part 2 of saving an obligation *)
-
 type progress =
   (* Resolution status of a program *)
   | Remain of int
@@ -78,6 +70,19 @@ type progress =
   | 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
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 98c7c0d077..686f52565c 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -38,29 +38,22 @@ module NamedDecl = Context.Named.Declaration
 
 type lemma_possible_guards = int list list
 
-type proof_ending =
-  | Admitted of
-      Names.Id.t *
-      Decl_kinds.goal_kind *
-      Entries.parameter_entry *
-      UState.t *
-      DeclareDef.Hook.t option
-
-  | Proved of
-      Proof_global.opacity_flag *
-      lident option *
-      Proof_global.proof_object *
-      DeclareDef.Hook.t option *
-      lemma_possible_guards
-
-type proof_terminator = (proof_ending -> unit) CEphemeron.key
+module Proof_ending = struct
+
+  type t =
+    | Regular
+    | End_obligation of DeclareObl.obligation_qed_info
+    | End_derive of { f : Id.t; name : Id.t }
+
+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 pf = { pf with proof = f pf.proof }
@@ -71,12 +64,9 @@ 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_info ps = ps.terminator, ps.hook, ps.compute_guard
+let get_info ps = ps.hook, ps.compute_guard, ps.proof_ending
 
 end
 (* Internal *)
@@ -209,7 +199,6 @@ let look_for_possibly_mutual_statements sigma = function
   | [] -> 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
@@ -316,15 +305,14 @@ let admit ?hook ctx (id,k,e) pl () =
   Declare.declare_univ_binders (ConstRef kn) pl;
   DeclareDef.Hook.call ?hook ctx [] (Global local) (ConstRef kn)
 
-(* Starting a goal *)
+let finish_admitted id k pe ctx hook =
+  let () = admit ?hook ctx (id,k,pe) (UState.universe_binders ctx) () in
+  Feedback.feedback Feedback.AddedAxiom
 
-let standard_proof_terminator =
+let finish_proved opaque idopt po hook compute_guard =
   let open Proof_global in
-  Internal.make_terminator begin function
-  | Admitted (id,k,pe,ctx,hook) ->
-    let () = admit ?hook ctx (id,k,pe) (UState.universe_binders ctx) () in
-    Feedback.feedback Feedback.AddedAxiom
-  | Proved (opaque,idopt, { id; entries=[const]; persistence; universes }, hook, compute_guard ) ->
+  match po with
+  | { id; entries=[const]; persistence; universes } ->
     let is_opaque, export_seff = match opaque with
       | Transparent -> false, true
       | Opaque      -> true, false
@@ -335,9 +323,8 @@ let standard_proof_terminator =
       | 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, _, hook,_) ->
-    CErrors.anomaly Pp.(str "[universe_proof_terminator] close_proof returned more than one proof term")
-  end
+  | _ ->
+    CErrors.anomaly Pp.(str "[standard_proof_terminator] close_proof returned more than one proof term")
 
 let initialize_named_context_for_proof () =
   let sign = Global.named_context () in
@@ -382,14 +369,17 @@ module Stack = struct
 
 end
 
-let start_lemma id ?pl kind sigma ?(terminator=standard_proof_terminator) ?(sign=initialize_named_context_for_proof()) ?(compute_guard=[]) ?hook c =
+(* 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; hook; compute_guard }
+  { proof ; hook; compute_guard; proof_ending = CEphemeron.create proof_ending }
 
-let start_dependent_lemma id ?pl kind ?(terminator=standard_proof_terminator) ?sign ?(compute_guard=[]) ?hook telescope =
+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; hook; compute_guard }
+  { proof; hook; compute_guard; proof_ending = CEphemeron.create proof_ending }
 
 let rec_tac_initializer finite guard thms snl =
   if finite then
@@ -480,23 +470,17 @@ let start_lemma_com ~program_mode ?inference_hook ?hook kind thms =
   start_lemma_with_initialization ?hook kind evd decl recguard thms snl
 
 (* Saving a proof *)
-
-let keep_admitted_vars = ref true
-
-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 }, (_, hook, _)) ->
+    | 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
@@ -504,8 +488,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, hook)
+      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
@@ -522,7 +506,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, _) :: _ ->
@@ -533,13 +517,64 @@ 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, lemma.hook)
-  in
-  CEphemeron.get lemma.terminator pe
+      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
 
-type proof_info = proof_terminator * DeclareDef.Hook.t option * lemma_possible_guards
+let default_info = None, [], CEphemeron.create Proof_ending.Regular
 
-let default_info = standard_proof_terminator, None, []
+let finish_derive ~f ~name ~idopt ~opaque ~entries =
+  (* 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. *)
+
+  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
+  (* 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 save_lemma_proved ?proof ?lemma ~opaque ~idopt =
   (* Invariant (uh) *)
@@ -550,10 +585,18 @@ let save_lemma_proved ?proof ?lemma ~opaque ~idopt =
     | 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; hook; compute_guard } = Option.get lemma in
-      Proof_global.close_proof ~opaque ~keep_body_ucst_separate:false (fun x -> x) proof, (terminator, hook, compute_guard)
+      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
-  let terminator, hook, compute_guard = proof_info in
-  CEphemeron.get terminator (Proved (opaque,idopt,proof_obj,hook,compute_guard))
+  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_derive ~f ~name ~idopt ~opaque ~entries:proof_obj.entries
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 961c1e41ef..51eada978a 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -11,9 +11,8 @@
 open Names
 open Decl_kinds
 
-(* 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
@@ -38,8 +37,6 @@ module Stack : sig
 
 end
 
-val standard_proof_terminator : 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
@@ -48,12 +45,21 @@ 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
+
 val start_lemma
   :  Id.t
   -> ?pl:UState.universe_decl
   -> goal_kind
   -> Evd.evar_map
-  -> ?terminator:proof_terminator
+  -> ?proof_ending:Proof_ending.t
   -> ?sign:Environ.named_context_val
   -> ?compute_guard:lemma_possible_guards
   -> ?hook:DeclareDef.Hook.t
@@ -64,8 +70,7 @@ val start_dependent_lemma
   :  Id.t
   -> ?pl:UState.universe_decl
   -> goal_kind
-  -> ?terminator:proof_terminator
-  -> ?sign:Environ.named_context_val
+  -> ?proof_ending:Proof_ending.t
   -> ?compute_guard:lemma_possible_guards
   -> ?hook:DeclareDef.Hook.t
   -> Proofview.telescope
@@ -112,29 +117,8 @@ val save_lemma_proved
   -> 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 *
-      DeclareDef.Hook.t option
-  | Proved of
-      Proof_global.opacity_flag *
-      lident option *
-      Proof_global.proof_object *
-      DeclareDef.Hook.t option *
-      lemma_possible_guards
-
-(** 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_info : t -> proof_info
-
-  (** Only needed by obligations, should be reified soon *)
-  val make_terminator : (proof_ending -> unit) -> proof_terminator
-  val apply_terminator : proof_terminator -> proof_ending -> unit
-
 end
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 9a34bda423..cd8d22ac9a 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -471,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 =
@@ -490,11 +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 = Lemmas.Internal.make_terminator
-      (obligation_terminator prg.prg_name num auto) 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) ~terminator ~hook 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
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 0749314301..d28eeb341d 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -14,9 +14,9 @@ Proof_using
 Egramcoq
 Metasyntax
 DeclareDef
-Lemmas
 DeclareObl
 Canonical
+Lemmas
 Class
 Auto_ind_decl
 Search