aboutsummaryrefslogtreecommitdiff
path: root/proofs/proof.mli
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/proof.mli')
-rw-r--r--proofs/proof.mli2
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