diff options
| -rw-r--r-- | checker/checker.ml | 2 | ||||
| -rw-r--r-- | ide/project_file.ml4 | 1 | ||||
| -rw-r--r-- | tools/coqc.ml | 25 | ||||
| -rw-r--r-- | tools/coqdep.ml | 7 | ||||
| -rw-r--r-- | toplevel/coqtop.ml | 4 |
5 files changed, 2 insertions, 37 deletions
diff --git a/checker/checker.ml b/checker/checker.ml index a13d529e8..da93685f9 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -331,8 +331,6 @@ let parse_args argv = | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem | ("-I"|"-include") :: [] -> usage () - | "-R" :: d :: "-as" :: p :: rem -> set_rec_include d p;parse rem - | "-R" :: d :: "-as" :: [] -> usage () | "-R" :: d :: p :: rem -> set_rec_include d p;parse rem | "-R" :: ([] | [_]) -> usage () diff --git a/ide/project_file.ml4 b/ide/project_file.ml4 index f66fd31c2..081094e2b 100644 --- a/ide/project_file.ml4 +++ b/ide/project_file.ml4 @@ -86,7 +86,6 @@ let rec process_cmd_line orig_dir ((project_file,makefile,install,opt) as opts) process_cmd_line orig_dir opts ((Include (CUnix.correct_path d orig_dir, lp)) :: l) r | "-I" :: d :: r -> process_cmd_line orig_dir opts ((MLInclude (CUnix.correct_path d orig_dir)) :: l) r - | "-R" :: p :: "-as" :: lp :: r | "-R" :: p :: lp :: r -> process_cmd_line orig_dir opts (RInclude (CUnix.correct_path p orig_dir,lp) :: l) r | ("-Q"|"-R"|"-I"|"-custom"|"-extra"|"-extra-phony") :: _ -> 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 = diff --git a/tools/coqdep.ml b/tools/coqdep.ml index aacfccfd7..0634f97fa 100644 --- a/tools/coqdep.ml +++ b/tools/coqdep.ml @@ -444,15 +444,8 @@ let rec parse = function | "-boot" :: ll -> option_boot := true; parse ll | "-sort" :: ll -> option_sort := true; parse ll | ("-noglob" | "-no-glob") :: ll -> option_noglob := true; parse ll - | "-I" :: r :: "-as" :: ln :: ll -> - add_rec_dir_no_import add_known r []; - add_rec_dir_no_import add_known r (split_period ln); - parse ll - | "-I" :: r :: "-as" :: [] -> usage () | "-I" :: r :: ll -> add_caml_dir r; parse ll | "-I" :: [] -> usage () - | "-R" :: r :: "-as" :: ln :: ll -> add_rec_dir_import add_known r (split_period ln); parse ll - | "-R" :: r :: "-as" :: [] -> usage () | "-R" :: r :: ln :: ll -> add_rec_dir_import add_known r (split_period ln); parse ll | "-Q" :: r :: ln :: ll -> add_rec_dir_no_import add_known r (split_period ln); parse ll | "-R" :: ([] | [_]) -> usage () diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 2aad417e8..bd0a79caf 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -443,10 +443,6 @@ let parse_args arglist = end |"-R" -> begin match rem with - | d :: "-as" :: [] -> error_missing_arg opt - | d :: "-as" :: p :: rem -> - warning "option -R * -as * deprecated, remove the -as"; - set_include d p true; args := rem | d :: p :: rem -> set_include d p true; args := rem | _ -> error_missing_arg opt end |