aboutsummaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
authorfilliatr2001-05-11 10:31:34 +0000
committerfilliatr2001-05-11 10:31:34 +0000
commit2a84370dce1e0f19cea46c473b1b2d236b72d9f8 (patch)
treec8152fafb4455b4b98991504bd9539db26b37d82 /toplevel
parent47b37874d6b0ec1b8a5f69655d4cab417ed4a05b (diff)
application patch Claudio
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1746 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/usage.mli4
1 files changed, 3 insertions, 1 deletions
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index 4322b0c9b0..c24ae331a1 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -12,7 +12,9 @@
val version : unit -> 'a
-(*s Prints the usage on the error output. *)
+(*s Prints the usage on the error output, preceeded by a user-provided message. *)
+val print_usage : string -> unit
+(*s Prints the usage on the error output. *)
val print_usage_coqtop : unit -> unit
val print_usage_coqc : unit -> unit