diff options
| -rw-r--r-- | doc/refman/RefMan-com.tex | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 21 | ||||
| -rw-r--r-- | man/coqide.1 | 8 | ||||
| -rw-r--r-- | man/coqtop.1 | 10 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 8 | ||||
| -rw-r--r-- | toplevel/usage.ml | 3 |
6 files changed, 6 insertions, 50 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index b010e6e18..3feabb228 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -116,12 +116,6 @@ Section~\ref{LongNames}). conventional version control management sub-directories named {\tt CVS} and {\tt \_darcs} are excluded. -\item[{\tt -is} {\em file}, {\tt -inputstate} {\em file}, {\tt -outputstate} {\em file}]\ - - Load at the beginning/Dump at the end a \Coq{} state from the file {\em file}. - - Incompatible with some not purely functional aspect of the code - \item[{\tt -nois}]\ Cause \Coq~to begin with an empty state. diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 8aa6df061..0a283776f 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -895,27 +895,6 @@ extra commands and end on a state $\num' \leq \num$ if necessary. The destination state label is unknown. \end{ErrMsgs} -\section{State files} - -\subsection[\tt Write State \str.]{\tt Write State \str.\comindex{Write State}} -Writes the current state into a file \str{} for -use in a further session. This file can be given as the {\tt - inputstate} argument of the commands {\tt coqtop} and {\tt coqc}. - -\begin{Variants} -\item {\tt Write State \ident}\\ - Equivalent to {\tt Write State "}{\ident}{\tt .coq"}. - The state is saved in the current directory (see Section~\ref{Pwd}). -\end{Variants} - -\subsection[\tt Restore State \str.]{\tt Restore State \str.\comindex{Restore State}} - Restores the state contained in the file \str. - -\begin{Variants} -\item {\tt Restore State \ident}\\ - Equivalent to {\tt Restore State "}{\ident}{\tt .coq"}. -\end{Variants} - \section{Quitting and debugging} \subsection[\tt Quit.]{\tt Quit.\comindex{Quit}} diff --git a/man/coqide.1 b/man/coqide.1 index 013c2ed7f..785a4a4c6 100644 --- a/man/coqide.1 +++ b/man/coqide.1 @@ -40,17 +40,9 @@ to logical .B \-src Add source directories in the include path. .TP -.BI \-is\ f ,\ \-inputstate\ f -Read state from -.IR f .coq. -.TP .B \-nois Start with an empty state. .TP -.BI \-outputstate\ f -Write state in file -.IR f .coq. -.TP .BI \-load\-ml\-object\ f Load ML object file .IR f . diff --git a/man/coqtop.1 b/man/coqtop.1 index 33982b117..068a5072b 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -47,20 +47,10 @@ set the toplevel name to be instead of Top .TP -.BI \-inputstate \ filename, \ \-is \ filename -read state from file -.I filename.coq - -.TP .B \-nois start with an empty initial state .TP -.BI \-outputstate filename -write state in file -.I filename.coq - -.TP .BI \-load\-ml\-object \ filename load ML object file .I filenname diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 4ad4b6a6c..43ffa762e 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -80,11 +80,15 @@ let unset_toplevel_name () = toplevel_name := None let remove_top_ml () = Mltop.remove () let inputstate = ref "" -let set_inputstate s = inputstate:=s +let set_inputstate s = + let () = msg_warning (str "The inputstate option is deprecated and discouraged.") in + inputstate:=s let inputstate () = if not (String.is_empty !inputstate) then intern_state !inputstate let outputstate = ref "" -let set_outputstate s = outputstate:=s +let set_outputstate s = + let () = msg_warning (str "The outputstate option is deprecated and discouraged.") in + outputstate:=s let outputstate () = if not (String.is_empty !outputstate) then extern_state !outputstate let set_include d p recursive implicit = 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\ |