From e8419bac30ab98527ec6b15d5a0f5c1035539ca5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 12 Feb 2019 02:41:00 +0100
Subject: [library] Remove `-boot` option.

The `-boot` option was used to:

- suppress loading of the rc_file
- allow to save modules with prefix `Coq`

There is no good reason disable saving of modules with `Coq` prefix by
default, thus we remove this option.

Fixes: #9575
---
 checker/checker.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'checker')

diff --git a/checker/checker.ml b/checker/checker.ml
index 4dac02210b..3c93ef7d36 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -192,7 +192,6 @@ let print_usage_channel co command =
 \n  -coqlib dir            set coqchk's standard library location\
 \n  -where                 print coqchk's standard library location and exit\
 \n  -v                     print coqchk version and exit\
-\n  -boot                  boot mode\
 \n  -o, --output-context   print the list of assumptions\
 \n  -m, --memory           print the maximum heap size\
 \n  -silent                disable trace of constants being checked\
@@ -320,8 +319,6 @@ let explain_exn = function
 let deprecated flag =
   Feedback.msg_warning (str "Deprecated flag " ++ quote (str flag))
 
-let boot_opt = ref false
-
 let parse_args argv =
   let rec parse = function
     | [] -> ()
@@ -358,7 +355,6 @@ let parse_args argv =
     | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
 
     | ("-v"|"--version") :: _ -> version ()
-    | "-boot" :: rem -> boot_opt := true; parse rem
     | ("-m" | "--memory") :: rem -> Check_stat.memory_stat := true; parse rem
     | ("-o" | "--output-context") :: rem ->
         Check_stat.output_context := true; parse rem
-- 
cgit v1.2.3