Merge PR #8716: Lemmas: Little simplification of artificially convoluted code

1 files changed, 6 insertions, 21 deletions

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index a99aace399..455dd86668 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -277,19 +277,10 @@ let save_remaining_recthms (locality,p,kind) norm univs body opaq i (id,(t_i,(_,
         let kn = declare_constant id ~local (DefinitionEntry const, k) in
         (locality,ConstRef kn,imps)
 
-let save_named ?export_seff proof =
-  let id,const,uctx,do_guard,persistence,hook = proof in
-  save ?export_seff id const uctx do_guard persistence hook
-
 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.")
 
-let save_anonymous ?export_seff proof save_ident =
-  let id,const,uctx,do_guard,persistence,hook = proof in
-  check_anonymity id save_ident;
-  save ?export_seff save_ident const uctx do_guard persistence hook
-
 (* Admitted *)
 
 let warn_let_as_axiom =
@@ -309,12 +300,6 @@ let admit (id,k,e) pl hook () =
 
 (* Starting a goal *)
 
-let get_proof proof do_guard hook opacity =
-  let (id,(const,univs,persistence)) =
-    Pfedit.cook_this_proof proof
-  in
-  id,{const with const_entry_opaque = opacity},univs,do_guard,persistence,hook
-
 let universe_proof_terminator compute_guard hook =
   let open Proof_global in
   make_terminator begin function
@@ -326,12 +311,12 @@ let universe_proof_terminator compute_guard hook =
         | Transparent -> false, true
         | Opaque      -> true, false
       in
-      let proof = get_proof proof compute_guard
-        (hook (Some (proof.Proof_global.universes))) is_opaque in
-      begin match idopt with
-      | None -> save_named ~export_seff proof
-      | Some { CAst.v = id } -> save_anonymous ~export_seff proof id
-      end
+      let (id,(const,univs,persistence)) = Pfedit.cook_this_proof proof in
+      let const = {const with const_entry_opaque = is_opaque} in
+      let id = match idopt with
+        | None -> id
+        | Some { CAst.v = save_id } -> check_anonymity id save_id; save_id in
+      save ~export_seff id const univs compute_guard persistence (hook (Some univs))
   end
 
 let standard_proof_terminator compute_guard hook =