aboutsummaryrefslogtreecommitdiffhomepage
path: root/ide/coqide.mli
diff options
context:
space:
mode:
Diffstat (limited to 'ide/coqide.mli')
-rw-r--r--ide/coqide.mli2
1 files changed, 0 insertions, 2 deletions
diff --git a/ide/coqide.mli b/ide/coqide.mli
index 39b4d9ae2..42dab9ec5 100644
--- a/ide/coqide.mli
+++ b/ide/coqide.mli
@@ -40,5 +40,3 @@ val set_signal_handlers : unit -> unit
(** Emergency saving of opened files as "foo.v.crashcoqide",
and exit (if the integer isn't 127). *)
val crash_save : int -> unit
-
-val check_for_geoproof_input : unit -> unit