aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/usage.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-08-16 20:37:59 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-08-16 22:17:45 +0200
commit6dd9e003c289a79b0656e7c6f2cc59935997370c (patch)
tree29bf3bccabd04d163eec29b14eee92caaea4712d /toplevel/usage.ml
parent2a3a190384cedc4dfdea5bdf1079d903db624cb8 (diff)
Removing documentation related to the deprecated State machinery.
Diffstat (limited to 'toplevel/usage.ml')
-rw-r--r--toplevel/usage.ml3
1 files changed, 0 insertions, 3 deletions
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index f31b4b933..eac46f566 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -30,9 +30,6 @@ let print_usage_channel co command =
\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 -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\
\n -no-compat-notations get an error when using compatibility notations\