aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-07-05 18:22:53 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-07-05 18:29:00 +0200
commitb2dd4dd979577e4f384750872f7f0e7f9bd8df94 (patch)
tree613c86859810558ec7127a47fc6469ec207b7ca5 /tools/coqdoc
parent82ed3089485ebe0b722d8505ddbd89d73570b8f9 (diff)
Revert "Merge remote-tracking branch 'github/pr/229' into trunk"
This reverts commit b2f8f9edd5c1bb0a9c8c4f4b049381b979d3e385, reversing changes made to da99355b4d6de31aec5a660f7afe100190a8e683. Hugo asked for more discussion on this topic, and it was not in the roadmap. I merged it prematurely because I thought there was a consensus. Also, I missed that it was changing coq_makefile. Sorry about that.
Diffstat (limited to 'tools/coqdoc')
-rw-r--r--tools/coqdoc/cdglobals.mli49
1 files changed, 0 insertions, 49 deletions
diff --git a/tools/coqdoc/cdglobals.mli b/tools/coqdoc/cdglobals.mli
deleted file mode 100644
index 2c9b3fb8e..000000000
--- a/tools/coqdoc/cdglobals.mli
+++ /dev/null
@@ -1,49 +0,0 @@
-type target_language = LaTeX | HTML | TeXmacs | Raw
-val target_language : target_language ref
-type output_t = StdOut | MultFiles | File of string
-val output_dir : string ref
-val out_to : output_t ref
-val out_channel : out_channel ref
-val ( / ) : string -> string -> string
-val coqdoc_out : string -> string
-val open_out_file : string -> unit
-val close_out_file : unit -> unit
-type glob_source_t = NoGlob | DotGlob | GlobFile of string
-val glob_source : glob_source_t ref
-val normalize_path : string -> string
-val normalize_filename : string -> string * string
-val guess_coqlib : unit -> string
-val header_trailer : bool ref
-val header_file : string ref
-val header_file_spec : bool ref
-val footer_file : string ref
-val footer_file_spec : bool ref
-val quiet : bool ref
-val light : bool ref
-val gallina : bool ref
-val short : bool ref
-val index : bool ref
-val multi_index : bool ref
-val index_name : string ref
-val toc : bool ref
-val page_title : string ref
-val title : string ref
-val externals : bool ref
-val coqlib : string ref
-val coqlib_path : string ref
-val raw_comments : bool ref
-val parse_comments : bool ref
-val plain_comments : bool ref
-val toc_depth : int option ref
-val lib_name : string ref
-val lib_subtitles : bool ref
-val interpolate : bool ref
-val inline_notmono : bool ref
-val charset : string ref
-val inputenc : string ref
-val latin1 : bool ref
-val utf8 : bool ref
-val set_latin1 : unit -> unit
-val set_utf8 : unit -> unit
-type coq_module = string
-type file = Vernac_file of string * coq_module | Latex_file of string