1 files changed, 7 insertions, 16 deletions
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index dfcb9c18..bc4b1321 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -28,8 +28,6 @@ let image = ref ""
 
 (* coqc options *)
 
-let specification = ref false
-let keep = ref false
 let verbose = ref false
 
 (* Verifies that a string starts by a letter and do not contain
@@ -104,28 +102,21 @@ let parse_args () =
   let rec parse (cfiles,args) = function
     | [] ->
 	List.rev cfiles, List.rev args
-    | "-i" :: rem ->
-	specification := true ; parse (cfiles,args) rem
-    | "-t" :: rem ->
-	keep := true ; parse (cfiles,args) rem
     | ("-verbose" | "--verbose") :: rem ->
 	verbose := true ; parse (cfiles,args) rem
-    | "-boot" :: rem ->
-	Flags.boot := true;
-	parse (cfiles, "-boot"::args) rem
-    | "-byte" :: rem ->
-	binary := "coqtop.byte"; parse (cfiles,args) rem
-    | "-opt" :: rem ->
-	binary := "coqtop.opt"; parse (cfiles,args) rem
     | "-image" :: f :: rem ->
 	image := f; parse (cfiles,args) rem
     | "-image" :: [] ->
 	usage ()
+    | "-byte" :: rem ->
+       binary := "coqtop.byte"; parse (cfiles,args) rem
+    | "-opt" :: rem ->
+       binary := "coqtop.opt"; parse (cfiles,args) rem
     | "-libdir" :: _ :: rem ->
-        print_string "Warning: option -libdir deprecated\n"; flush stdout;
+        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\n";flush stdout;
+        print_string "Warning: option -db/-debugger deprecated and ignored\n";flush stdout;
         parse (cfiles,args) rem
 
     | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
@@ -150,7 +141,7 @@ let parse_args () =
     | "-R" :: s :: "-as" :: [] -> usage ()
     | "-R" :: s :: t :: rem -> parse (cfiles,t::s::"-R"::args) rem
 
-    | ("-notactics"|"-debug"|"-nolib"
+    | ("-notactics"|"-debug"|"-nolib"|"-boot"
       |"-batch"|"-nois"|"-noglob"|"-no-glob"
       |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
       |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"