diff options
Diffstat (limited to 'tools/coqdoc/output.mli')
| -rw-r--r-- | tools/coqdoc/output.mli | 31 |
1 files changed, 3 insertions, 28 deletions
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index 2195fa53..87b311f3 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -6,35 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: output.mli,v 1.3.2.1 2004/07/16 19:31:47 herbelin Exp $ i*) +(*i $Id: output.mli 8669 2006-03-28 17:34:15Z notin $ i*) +open Cdglobals open Index -type target_language = LaTeX | HTML | TeXmacs - -val target_language : target_language ref - -val set_out_file : string -> unit -val output_dir : string ref -val close : unit -> unit - -val quiet : bool ref -val short : bool ref -val light : bool ref -val header_trailer : bool ref -val index : bool ref -val multi_index : bool ref -val toc : bool ref -val title : string ref -val externals : bool ref -val coqlib : string ref -val raw_comments : bool ref - -val charset : string ref -val inputenc : string ref -val set_latin1 : unit -> unit -val set_utf8 : unit -> unit - val add_printing_token : string -> string option * string option -> unit val remove_printing_token : string -> unit @@ -45,8 +21,6 @@ val trailer : unit -> unit val push_in_preamble : string -> unit -val dump_file : string -> unit - val start_module : unit -> unit val start_doc : unit -> unit @@ -88,5 +62,6 @@ val stop_latex_math : unit -> unit val start_verbatim : unit -> unit val stop_verbatim : unit -> unit +val make_multi_index : unit -> unit val make_index : unit -> unit val make_toc : unit -> unit |