Merge PR #8703: [vernac] Remove unused `start_hook` `save_hook` from Lemmas.

2 files changed, 0 insertions, 15 deletions

diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 4f0bf1b5d2..bbefd2dfe7 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -277,9 +277,6 @@ 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_hook = ref ignore
-let set_save_hook f = save_hook := f
-
 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
@@ -312,10 +309,6 @@ let admit (id,k,e) pl hook () =
 
 (* Starting a goal *)
 
-let start_hook = ref ignore
-let set_start_hook = (:=) start_hook
-
-
 let get_proof proof do_guard hook opacity =
   let (id,(const,univs,persistence)) =
     Pfedit.cook_this_proof proof
@@ -362,7 +355,6 @@ let start_proof id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=
     | Some sign -> sign
     | None -> initialize_named_context_for_proof ()
   in
-  !start_hook c;
   Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
 
 let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_guard=[]) hook =
@@ -375,7 +367,6 @@ let start_proof_univs id ?pl kind sigma ?terminator ?sign c ?init_tac ?(compute_
     | Some sign -> sign
     | None -> initialize_named_context_for_proof ()
   in
-  !start_hook c;
   Pfedit.start_proof id ?pl kind sigma sign c ?init_tac terminator
 
 let rec_tac_initializer finite guard thms snl =
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 62b25946d9..d8e337c09c 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -18,9 +18,6 @@ val mk_hook :
 val call_hook :
   Future.fix_exn -> 'a declaration_hook -> Decl_kinds.locality -> GlobRef.t -> 'a
 
-(** A hook start_proof calls on the type of the definition being started *)
-val set_start_hook : (EConstr.types -> unit) -> unit
-
 val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
   ?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
   ?sign:Environ.named_context_val -> EConstr.types ->
@@ -63,7 +60,4 @@ val initialize_named_context_for_proof : unit -> Environ.named_context_val
 
 (** {6 ... } *)
 
-(** A hook the next three functions pass to cook_proof *)
-val set_save_hook : (Proof.t -> unit) -> unit
-
 val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> unit