Remove some unused functions.

Note: they do not even seem to have a debugging purpose, so better remove
them before they bitrot.

3 files changed, 0 insertions, 24 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index a60f327b4..268a95a33 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -99,9 +99,6 @@ let display_coqtop_answer cmd lines =
      "Command was: "^cmd^"\n"^
      "Answer was: "^(String.concat "\n  " lines))
 
-let check_remaining_opt arg =
-  if arg <> "" && arg.[0] = '-' then fatal_error_popup ("Illegal option: "^arg)
-
 let rec filter_coq_opts args =
   let argstr = String.concat " " (List.map Filename.quote args) in
   let cmd = Filename.quote (coqtop_path ()) ^" -nois -filteropts " ^ argstr in
@@ -200,8 +197,6 @@ module GlibMainLoop = struct
   let read_all = Ideutils.io_read_all
   let async_chan_of_file fd = Glib.Io.channel_of_descr fd
   let async_chan_of_socket s = !gio_channel_of_descr_socket s
-  let add_timeout ~sec callback =
-    ignore(Glib.Timeout.add ~ms:(sec * 1000) ~callback)
 end
 
 module CoqTop = Spawn.Async(GlibMainLoop)
diff --git a/ide/document.ml b/ide/document.ml
index 41d5a7564..bb431e791 100644
--- a/ide/document.ml
+++ b/ide/document.ml
@@ -124,12 +124,6 @@ let context d =
   let pair _ x y = try Option.get x, y with Option.IsNone -> assert false in
   List.map (flat pair true) top, List.map (flat pair true) bot
 
-let iter d f =
-  let a, s, b = to_lists d in
-  List.iter (flat f false) a;
-  List.iter (flat f true)  s;
-  List.iter (flat f false) b
-  
 let stateid_opt_equal = Option.equal Stateid.equal
 
 let is_in_focus d id =
diff --git a/ide/wg_ProofView.ml b/ide/wg_ProofView.ml
index 148add6e9..642a57787 100644
--- a/ide/wg_ProofView.ml
+++ b/ide/wg_ProofView.ml
@@ -114,19 +114,6 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals hints = match goals with
                          (Some Tags.Proof.goal)));
       ignore(proof#scroll_to_mark ~use_align:true ~yalign:0.95 `INSERT)
 
-let mode_cesar (proof : #GText.view_skel) = function
-  | [] -> assert false
-  | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; } :: _ ->
-      proof#buffer#insert "    *** Declarative Mode ***\n";
-      List.iter
-        (fun hyp -> insert_xml proof#buffer hyp; proof#buffer#insert "\n")
-        hyps;
-      proof#buffer#insert "______________________________________\n";
-      proof#buffer#insert "thesis := \n ";
-      insert_xml proof#buffer cur_goal;
-      proof#buffer#insert "\n";
-      ignore (proof#scroll_to_iter (proof#buffer#get_iter_at_mark `INSERT))
-
 let rec flatten = function
 | [] -> []
 | (lg, rg) :: l ->