diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-14 18:58:03 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-07-27 12:36:13 +0200 |
| commit | 624dc13d0e80dcde22beecd3c80e68037899c287 (patch) | |
| tree | cf614a1ac45fbf1a5800e242434135d944e2a84c /toplevel | |
| parent | 2a7ba998bf7d2c461fdbd8b710b7124395bafaa2 (diff) | |
[toplevel] Remove long ago deprecated and NOOP options.
Minor clean up, no sense in having these as they do nothing.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/coqtop.ml | 17 |
1 files changed, 0 insertions, 17 deletions
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 515552fe7..2cf8c7c2a 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -138,8 +138,6 @@ let set_toplevel_name dir = if Names.DirPath.is_empty dir then user_err Pp.(str "Need a non empty toplevel module name"); toplevel_name := dir -let remove_top_ml () = Mltop.remove () - let warn_deprecated_inputstate = CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" (fun () -> strbrk "The inputstate option is deprecated and discouraged.") @@ -589,21 +587,6 @@ let parse_args arglist = |"-where" -> print_where := true |"-xml" -> Flags.xml_export := true - (* Deprecated options *) - |"-byte" -> warning "option -byte deprecated, call with .byte suffix" - |"-opt" -> warning "option -opt deprecated, call with .opt suffix" - |"-full" -> warning "option -full deprecated" - |"-notactics" -> warning "Obsolete option \"-notactics\"."; remove_top_ml () - |"-emacs-U" -> - warning "Obsolete option \"-emacs-U\", use -emacs instead."; set_emacs () - |"-v7" -> user_err Pp.(str "This version of Coq does not support v7 syntax") - |"-v8" -> warning "Obsolete option \"-v8\"." - |"-lazy-load-proofs" -> warning "Obsolete option \"-lazy-load-proofs\"." - |"-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 end; |