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

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

6 files changed, 15 insertions, 75 deletions

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