diff options
| author | Emilio Jesus Gallego Arias | 2019-07-01 04:00:11 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-11 18:19:12 +0200 |
| commit | 2576fee1798b753161a730244c8d4d701e8a4641 (patch) | |
| tree | e07fa6b7e015b08565fd73c9f36c4dcf8cc2cfed /proofs/proof.mli | |
| parent | efe7108a0ae32faeb674cc5d97e6fa955a1dccd8 (diff) | |
[proof] Minor cleanup in proof.ml
Diffstat (limited to 'proofs/proof.mli')
| -rw-r--r-- | proofs/proof.mli | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/proofs/proof.mli b/proofs/proof.mli index 7e535a258c..9973df492d 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -176,8 +176,6 @@ val maximal_unfocus : 'a focus_kind -> t -> t (*** Commands ***) -val in_proof : t -> (Evd.evar_map -> 'a) -> 'a - (* Remove all the goals from the shelf and adds them at the end of the focused goals. *) val unshelve : t -> t |