aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--checker/checker.ml2
-rw-r--r--ide/project_file.ml41
-rw-r--r--tools/coqc.ml25
-rw-r--r--tools/coqdep.ml7
-rw-r--r--toplevel/coqtop.ml4
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