From 4264aec518d5407f345c58e18e014e15e9ae96af Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 5 Jan 2021 11:34:35 +0100 Subject: [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 --- sysinit/usage.mli | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 sysinit/usage.mli (limited to 'sysinit/usage.mli') 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 *) +(* 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 -- cgit v1.2.3