aboutsummaryrefslogtreecommitdiff
path: root/toplevel/usage.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/usage.ml')
-rw-r--r--toplevel/usage.ml2
1 files changed, 0 insertions, 2 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 956a402617..38ceacf5ec 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -36,8 +36,6 @@ let print_usage_channel co command =
\n -noinit start without loading the Init library\
\n -nois (idem)\
\n -compat X.Y provides compatibility support for Coq version X.Y\
-\n -verbose-compat-notations be warned when using compatibility notations\
-\n -no-compat-notations get an error when using compatibility notations\
\n\
\n -load-ml-object f load ML object file f\
\n -load-ml-source f load ML file f\