diff options
Diffstat (limited to 'proofs/proof_global.mli')
| -rw-r--r-- | proofs/proof_global.mli | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 53aab2b9db..8dbb63739f 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -69,12 +69,6 @@ val close_proof : unit -> exception NoSuchProof -val suspend : unit -> unit -val resume_last : unit -> unit - -val resume : Names.identifier -> unit -(** @raise NoSuchProof if it doesn't find one. *) - (** Runs a tactic on the current proof. Raises [NoCurrentProof] is there is no current proof. *) val run_tactic : unit Proofview.tactic -> unit |