From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 tools/coqc.ml | 29 ++++-------------------------
 1 file changed, 4 insertions(+), 25 deletions(-)

(limited to 'tools/coqc.ml')

diff --git a/tools/coqc.ml b/tools/coqc.ml
index b7910e13..b12d4871 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 ()
@@ -99,13 +88,12 @@ let parse_args () =
 
 (* Options for coqtop : a) options with 0 argument *)
 
-    | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time"
+    | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac"
       |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob"
       |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet"
       |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit"
       |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs"
       |"-impredicative-set"|"-vm"|"-native-compiler"
-      |"-verbose-compat-notations"|"-no-compat-notations"
       |"-indices-matter"|"-quick"|"-type-in-type"
       |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
       as o) :: rem ->
@@ -118,27 +106,18 @@ let parse_args () =
       |"-load-ml-source"|"-require"|"-load-ml-object"
       |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top"
       |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w"
+      |"-o"|"-profile-ltac-cutoff" 
       as o) :: rem ->
 	begin
 	  match rem with
 	    | 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 =
-- 
cgit v1.2.3