diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-06 15:08:08 +0100 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2016-01-06 15:08:08 +0100 |
| commit | 6599e31f04b6e8980de72e9d3913b70c04b6698c (patch) | |
| tree | f28177b60a7f537bde0f4763c320e08529bddbb3 /tools/coqc.ml | |
| parent | d0d46d9c5a93de25ecf0202a0ab3dbd83f1ed693 (diff) | |
Remove deprecated command-line options such as "-as".
Diffstat (limited to 'tools/coqc.ml')
| -rw-r--r-- | tools/coqc.ml | 25 |
1 files changed, 2 insertions, 23 deletions
diff --git a/tools/coqc.ml b/tools/coqc.ml index e7239da68..034c9b7f4 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -70,17 +70,6 @@ let parse_args () = | "-byte" :: rem -> binary := "coqtop.byte"; parse (cfiles,args) rem | "-opt" :: rem -> binary := "coqtop"; parse (cfiles,args) rem -(* Obsolete options *) - - | "-libdir" :: _ :: rem -> - print_string "Warning: option -libdir deprecated and ignored\n"; - flush stdout; - parse (cfiles,args) rem - | ("-db"|"-debugger") :: rem -> - print_string "Warning: option -db/-debugger deprecated and ignored\n"; - flush stdout; - parse (cfiles,args) rem - (* Informative options *) | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage () @@ -124,21 +113,11 @@ let parse_args () = | s :: rem' -> parse (cfiles,s::o::args) rem' | [] -> usage () end + | ("-I"|"-include" as o) :: s :: rem -> parse (cfiles,s::o::args) rem (* Options for coqtop : c) options with 1 argument and possibly more *) - | ("-I"|"-include" as o) :: rem -> - begin - match rem with - | s :: "-as" :: t :: rem' -> parse (cfiles,t::"-as"::s::o::args) rem' - | s :: "-as" :: [] -> usage () - | s :: rem' -> parse (cfiles,s::o::args) rem' - | [] -> usage () - end - | "-R" :: s :: "-as" :: t :: rem -> parse (cfiles,t::"-as"::s::"-R"::args) rem - | "-R" :: s :: "-as" :: [] -> usage () - | "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem - | "-Q" :: s :: t :: rem -> parse (cfiles,t::s::"-Q"::args) rem + | ("-R"|"-Q" as o) :: s :: t :: rem -> parse (cfiles,t::s::o::args) rem | ("-schedule-vio-checking" |"-check-vio-tasks" | "-schedule-vio2vo" as o) :: s :: rem -> let nodash, rem = |