aboutsummaryrefslogtreecommitdiff
path: root/toplevel/usage.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/usage.ml')
-rw-r--r--toplevel/usage.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 2ddd42d7bd..4751f7e326 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -27,9 +27,10 @@ let print_usage_channel co command =
\n -notop set the toplevel name to be the empty logical path\
\n -exclude-dir f exclude subdirectories named f for option -R\
\n\
+\n -noinit start without loading the Init library\
+\n -nois (idem)\
\n -inputstate f read state from file f.coq\
\n -is f (idem)\
-\n -nois start with an empty state\
\n -outputstate f write state in file f.coq\
\n -compat X.Y provides compatibility support for Coq version X.Y\
\n -verbose-compat-notations be warned when using compatibility notations\