From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:04:58 +0200
Subject: Remove some unused values and types

---
 ide/coqOps.ml   |  3 ---
 ide/ideutils.ml | 11 -----------
 2 files changed, 14 deletions(-)

(limited to 'ide')

diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index 259557f407..b180aa5569 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -128,9 +128,6 @@ end = struct
 end
 open SentenceId
 
-let log_pp msg : unit task =
-  Coq.lift (fun () -> Minilib.log_pp msg)
-
 let log msg : unit task =
   Coq.lift (fun () -> Minilib.log msg)
 
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index d7d38a5ec2..a08ab07b5f 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -35,17 +35,6 @@ let flash_info =
   let flash_context = status#new_context ~name:"Flash" in
     (fun ?(delay=5000) s -> flash_context#flash ~delay s)
 
-let xml_to_string xml =
-  let open Xml_datatype in
-  let buf = Buffer.create 1024 in
-  let rec iter = function
-  | PCData s -> Buffer.add_string buf s
-  | Element (_, _, children) ->
-    List.iter iter children
-  in
-  let () = iter xml in
-  Buffer.contents buf
-
 let insert_with_tags (buf : #GText.buffer_skel) mark rmark tags text =
   (** FIXME: LablGTK2 does not export the C insert_with_tags function, so that
       it has to reimplement its own helper function. Unluckily, it relies on
-- 
cgit v1.2.3