diff options
Diffstat (limited to 'toplevel/usage.mli')
| -rw-r--r-- | toplevel/usage.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/toplevel/usage.mli b/toplevel/usage.mli index fb973e3baf..37d96cfa82 100644 --- a/toplevel/usage.mli +++ b/toplevel/usage.mli @@ -21,3 +21,6 @@ val print_usage_coqc : unit -> unit (*s Prints the configuration information *) val print_config : unit -> unit + +(*s Prints the header *) +val print_header : unit -> unit |