diff options
Diffstat (limited to 'tools/coqdoc/output.mli')
| -rw-r--r-- | tools/coqdoc/output.mli | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli index b7a8d4d858..4088fdabf7 100644 --- a/tools/coqdoc/output.mli +++ b/tools/coqdoc/output.mli @@ -41,9 +41,6 @@ val end_comment : unit -> unit val start_coq : unit -> unit val end_coq : unit -> unit -val start_code : unit -> unit -val end_code : unit -> unit - val start_inline_coq : unit -> unit val end_inline_coq : unit -> unit |