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
---
 tools/coq_dune.ml | 2 +-
 tools/coq_tex.ml  | 3 ---
 2 files changed, 1 insertion(+), 4 deletions(-)

(limited to 'tools')

diff --git a/tools/coq_dune.ml b/tools/coq_dune.ml
index 68371edcb1..62a871aa0e 100644
--- a/tools/coq_dune.ml
+++ b/tools/coq_dune.ml
@@ -186,7 +186,7 @@ let pp_vo_dep dir fmt vo =
   (* We explicitly include the location of coqlib to avoid tricky issues with coqlib location *)
   let libflag = "-coqlib %{project_root}" in
   (* The final build rule *)
-  let action = sprintf "(chdir %%{project_root} (run coqc -boot %s %s %s %s))" libflag eflag cflag source in
+  let action = sprintf "(chdir %%{project_root} (run coqc -q %s %s %s %s))" libflag eflag cflag source in
   let all_targets = gen_coqc_targets vo in
   pp_rule fmt all_targets deps action
 
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index 0ffa5bd7e4..c6d3551561 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -259,8 +259,6 @@ let parse_cl () =
 	"           Coq parts are written between 2 horizontal lines";
 	"-small", Arg.Set small,
 	"           Coq parts are written in small font";
-	"-boot", Arg.Set boot,
-	"            Launch coqtop with the -boot option"
       ]
       (fun s -> files := s :: !files)
       "coq-tex [options] file ..."
@@ -279,7 +277,6 @@ let find_coqtop () =
 let _ =
   parse_cl ();
   if !image = "" then image := Filename.quote (find_coqtop ());
-  if !boot then image := !image ^ " -boot";
   if Sys.command (!image ^ " -batch -silent") <> 0 then begin
     Printf.printf "Error: ";
     let _ = Sys.command (!image ^ " -batch") in
-- 
cgit v1.2.3