From 2576fee1798b753161a730244c8d4d701e8a4641 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 1 Jul 2019 04:00:11 +0200
Subject: [proof] Minor cleanup in proof.ml

---
 proofs/proof.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'proofs/proof.mli')

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
-- 
cgit v1.2.3