diff options
| -rw-r--r-- | doc/refman/RefMan-com.tex | 4 | ||||
| -rw-r--r-- | lib/flags.ml | 2 | ||||
| -rw-r--r-- | lib/flags.mli | 2 | ||||
| -rw-r--r-- | man/coqtop.1 | 5 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 2 | ||||
| -rw-r--r-- | toplevel/usage.ml | 2 |
6 files changed, 1 insertions, 16 deletions
diff --git a/doc/refman/RefMan-com.tex b/doc/refman/RefMan-com.tex index 20088fd72..87ec076fa 100644 --- a/doc/refman/RefMan-com.tex +++ b/doc/refman/RefMan-com.tex @@ -187,10 +187,6 @@ Section~\ref{LongNames}). it in {\em file}{\tt .beautified} in order to get old-fashion syntax/definitions/notations. -\item[{\tt -quality}] - - Improve the legibility of the proof terms produced by some tactics. - \item[{\tt -emacs}, {\tt -ide-slave}]\ Start a special main loop to communicate with ide. diff --git a/lib/flags.ml b/lib/flags.ml index 5fba48dd6..7fed95100 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -64,8 +64,6 @@ let profile = false let print_emacs = ref false -let term_quality = ref false - let xml_export = ref false let ide_slave = ref false diff --git a/lib/flags.mli b/lib/flags.mli index b5947c48f..c1e5a9dbd 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -28,8 +28,6 @@ val profile : bool val print_emacs : bool ref -val term_quality : bool ref - val xml_export : bool ref val ide_slave : bool ref diff --git a/man/coqtop.1 b/man/coqtop.1 index 8006d4993..33982b117 100644 --- a/man/coqtop.1 +++ b/man/coqtop.1 @@ -168,11 +168,6 @@ export XML files either to the hierarchy rooted in the directory $COQ_XML_LIBRARY_ROOT (if set) or to stdout (if unset) -.TP -.B \-quality -improve the legibility of the proof terms produced by -some tactics - .SH SEE ALSO .BR coqc (1), diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 1f4bd4bbf..a4770b348 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -389,7 +389,6 @@ let parse_args arglist = |"-notop" -> unset_toplevel_name () |"-output-context" -> output_context := true |"-q" -> no_load_rc () - |"-quality" -> term_quality := true; no_load_rc () |"-quiet"|"-silent" -> Flags.make_silent true |"-quick" -> Flags.compilation_mode := BuildVi |"-time" -> Flags.time := true @@ -413,6 +412,7 @@ let parse_args arglist = |"-dont-load-proofs" -> warning "Obsolete option \"-dont-load-proofs\"." |"-force-load-proofs" -> warning "Obsolete option \"-force-load-proofs\"." |"-unsafe" -> warning "Obsolete option \"-unsafe\"."; ignore (next ()) + |"-quality" -> warning "Obsolete option \"-quality\"." (* Unknown option *) | s -> extras := s :: !extras diff --git a/toplevel/usage.ml b/toplevel/usage.ml index 19dbfef19..f31b4b933 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -67,8 +67,6 @@ let print_usage_channel co command = \n -xml export XML files either to the hierarchy rooted in\ \n the directory $COQ_XML_LIBRARY_ROOT (if set) or to\ \n stdout (if unset)\ -\n -quality improve the legibility of the proof terms produced by\ -\n some tactics\ \n -time display the time taken by each command\ \n -h, --help print this list of options\ \n --help-XML-protocol print the documentation of the XML protocol used by CoqIDE\ |