diff options
| -rw-r--r-- | vernac/lemmas.ml | 9 | ||||
| -rw-r--r-- | vernac/lemmas.mli | 6 |
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 |