From 624dc13d0e80dcde22beecd3c80e68037899c287 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 14 Jun 2017 18:58:03 +0200
Subject: [toplevel] Remove long ago deprecated and NOOP options.

Minor clean up, no sense in having these as they do nothing.
---
 tools/coqc.ml     | 9 ++++-----
 tools/coqmktop.ml | 2 --
 2 files changed, 4 insertions(+), 7 deletions(-)

(limited to 'tools')

diff --git a/tools/coqc.ml b/tools/coqc.ml
index 5da203742c..66aee56bd4 100644
--- a/tools/coqc.ml
+++ b/tools/coqc.ml
@@ -91,11 +91,10 @@ let parse_args () =
 
 (* Options for coqtop : a) options with 0 argument *)
 
-    | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac"
+    | ("-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"
+      |"-q"|"-profile"|"-just-parsing"|"-echo" |"-quiet"
+      |"-silent"|"-m"|"-xml"|"-beautify"|"-strict-implicit"
       |"-impredicative-set"|"-vm"|"-native-compiler"
       |"-indices-matter"|"-quick"|"-type-in-type"
       |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch"
@@ -110,7 +109,7 @@ 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" 
+      |"-o"|"-profile-ltac-cutoff"
       as o) :: rem ->
 	begin
 	  match rem with
diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml
index 30e098df59..28a3c791cb 100644
--- a/tools/coqmktop.ml
+++ b/tools/coqmktop.ml
@@ -175,8 +175,6 @@ let parse_args () =
     | "-top" :: rem -> top := true ; parse (op,fl) rem
     | "-no-start" :: rem -> no_start:=true; parse (op, fl) rem
     | "-echo" :: rem -> echo := true ; parse (op,fl) rem
-    | ("-v8"|"-full" as o) :: rem ->
-	Printf.eprintf "warning: option %s deprecated\n" o; parse (op,fl) rem
 
     (* Extra options with arity 0 or 1, directly passed to ocamlc/ocamlopt *)
     | ("-noassert"|"-compact"|"-g"|"-p"|"-thread"|"-dtypes" as o) :: rem ->
-- 
cgit v1.2.3