aboutsummaryrefslogtreecommitdiff
path: root/sysinit/usage.mli
diff options
context:
space:
mode:
authorEnrico Tassi2021-01-05 11:34:35 +0100
committerEnrico Tassi2021-01-27 09:45:49 +0100
commit4264aec518d5407f345c58e18e014e15e9ae96af (patch)
tree03209892ae2549f171af39efa5d6925b745d54ec /sysinit/usage.mli
parent4390b6907b3d07793c2e8f9e7ad3cc38d9488711 (diff)
[sysinit] new component for system initialization
This component holds the code for initializing Coq: - parsing arguments not specific to the toplevel - initializing all components from vernac downwards (no stm) This commit moves stm specific arguments parsing to stm/stmargs.ml
Diffstat (limited to 'sysinit/usage.mli')
-rw-r--r--sysinit/usage.mli28
1 files changed, 28 insertions, 0 deletions
diff --git a/sysinit/usage.mli b/sysinit/usage.mli
new file mode 100644
index 0000000000..2d1a8e94cc
--- /dev/null
+++ b/sysinit/usage.mli
@@ -0,0 +1,28 @@
+(************************************************************************)
+(* * The Coq Proof Assistant / The Coq Development Team *)
+(* v * Copyright INRIA, CNRS and contributors *)
+(* <O___,, * (see version control and CREDITS file for authors & dates) *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+(** {6 Prints the version number on the standard output. } *)
+
+val version : unit -> unit
+val machine_readable_version : unit -> unit
+
+(** {6 extra arguments or options to print when asking usage for a
+ given executable. } *)
+
+type specific_usage = {
+ executable_name : string;
+ extra_args : string;
+ extra_options : string;
+}
+
+(** {6 Prints the generic part and specific part of usage for a
+ given executable. } *)
+
+val print_usage : out_channel -> specific_usage -> unit