From f461e7657cab9917c5b405427ddba3d56f197efb Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 8 May 2016 18:59:55 +0200
Subject: Removing dead code and unused opens.

---
 tools/coqdoc/cpretty.mll |  8 +-------
 tools/coqdoc/index.ml    | 26 --------------------------
 tools/coqdoc/output.ml   |  3 +--
 3 files changed, 2 insertions(+), 35 deletions(-)

(limited to 'tools/coqdoc')

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index 431080c6b..81c01f29d 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -75,7 +75,7 @@
     let stop_env () = if !r then stop (); r := false in
       (fun x -> !r), start_env, stop_env
       
-  let in_emph, start_emph, stop_emph = in_env Output.start_emph Output.stop_emph
+  let _, start_emph, stop_emph = in_env Output.start_emph Output.stop_emph
   let in_quote, start_quote, stop_quote = in_env Output.start_quote Output.stop_quote
 
   let url_buffer = Buffer.create 40
@@ -111,12 +111,6 @@
     Cdglobals.gallina := s.st_gallina;
     Cdglobals.light := s.st_light
 
-  let without_ref r f x = save_state (); r := false; f x; restore_state ()
-
-  let without_gallina = without_ref Cdglobals.gallina
-
-  let without_light = without_ref Cdglobals.light
-
   let begin_show () = save_state (); Cdglobals.gallina := false; Cdglobals.light := false
   let end_show () = restore_state ()
 
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 47acc7b43..9be791a8d 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -77,32 +77,6 @@ let find m l = Hashtbl.find reftable (m, l)
 
 let find_string m s = let (m,s,t) = Hashtbl.find byidtable s in Ref (m,s,t)
 
-(*s Manipulating path prefixes *)
-
-type stack = string list
-
-let rec string_of_stack st =
-  match st with
-    | [] -> ""
-    | x::[] -> x
-    | x::tl -> (string_of_stack tl) ^ "." ^ x
-
-let empty_stack = []
-
-let module_stack = ref empty_stack
-let section_stack = ref empty_stack
-
-let push st p = st := p::!st
-let pop st =
-  match !st with
-    | [] -> ()
-    | _::tl -> st := tl
-
-let head st =
-  match st with
-    | [] -> ""
-    | x::_ -> x
-
 (* Coq modules *)
 
 let split_sp s =
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 2b2690968..82d3d62b5 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -953,7 +953,7 @@ module TeXmacs = struct
 
   (*s Latex preamble *)
 
-  let (preamble : string Queue.t) =
+  let (_ : string Queue.t) =
     in_doc := false; Queue.create ()
 
   let header () =
@@ -1122,7 +1122,6 @@ module Raw = struct
     for i = 0 to String.length s - 1 do char s.[i] done
 
   let start_module () = ()
-  let end_module () = ()
 
   let start_latex_math () = ()
   let stop_latex_math () = ()
-- 
cgit v1.2.3