diff options
Diffstat (limited to 'tools/coqdoc/output.mli')
| -rw-r--r-- | tools/coqdoc/output.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index f8a25285c..1ccbac2f9 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -60,9 +60,10 @@ 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 symbol : string -> loc -> unit val proofbox : unit -> unit |