aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-08 18:59:55 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-05-08 19:59:03 +0200
commitf461e7657cab9917c5b405427ddba3d56f197efb (patch)
tree467ac699f78d0360b05174238aeb1177da892503 /tools/coqdoc
parent9fe0471ef0127e9301d0450aacaeb1690abb82ad (diff)
Removing dead code and unused opens.
Diffstat (limited to 'tools/coqdoc')
-rw-r--r--tools/coqdoc/cpretty.mll8
-rw-r--r--tools/coqdoc/index.ml26
-rw-r--r--tools/coqdoc/output.ml3
3 files changed, 2 insertions, 35 deletions
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 () = ()