1 files changed, 16 insertions, 3 deletions
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 75c7ccf8..d836f6b3 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: output.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
+(*i $Id$ i*)
 
 open Cdglobals
 open Index
@@ -16,7 +16,8 @@ val initialize : unit -> unit
 val add_printing_token : string -> string option * string option -> unit
 val remove_printing_token : string -> unit
 
-val set_module : coq_module -> unit
+val set_module : coq_module -> string option -> unit
+val get_module : bool -> string
 
 val header : unit -> unit
 val trailer : unit -> unit
@@ -28,6 +29,9 @@ val start_module : unit -> unit
 val start_doc : unit -> unit
 val end_doc : unit -> unit
 
+val start_emph : unit -> unit
+val stop_emph : unit -> unit
+
 val start_comment : unit -> unit
 val end_comment : unit -> unit
 
@@ -40,6 +44,9 @@ val end_code : unit -> unit
 val start_inline_coq : unit -> unit
 val end_inline_coq : unit -> unit
 
+val start_inline_coq_block : unit -> unit
+val end_inline_coq_block : unit -> unit
+
 val indentation : int -> unit
 val line_break : unit -> unit
 val paragraph : unit -> unit
@@ -48,12 +55,18 @@ val empty_line_of_code : unit -> unit
 val section : int -> (unit -> unit) -> unit
 
 val item : int -> unit
+val stop_item : unit -> unit
+val reach_item_level : int -> unit
 
 val rule : unit -> unit
 
+val nbsp : unit -> unit
 val char : char -> unit
 val ident : string -> loc -> unit
-val symbol : string -> unit
+val sublexer : char -> loc -> unit
+val initialize : unit -> unit
+
+val proofbox : unit -> unit
 
 val latex_char : char -> unit
 val latex_string : string -> unit