[lib] [flags] Move coqlib handling out of `Flags`

The relevant logic is already in `Envars`, so it makes sense to make
it private and don't expose the low-level implementation of the logic.

7 files changed, 17 insertions, 16 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index fd2725c859..d3d114d7d7 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -321,8 +321,7 @@ let parse_args argv =
     | "-coqlib" :: s :: rem ->
       if not (exists_dir s) then 
 	fatal_error (str "Directory '" ++ str s ++ str "' does not exist") false;
-      Flags.coqlib := s;
-      Flags.coqlib_spec := true;
+      Envars.set_user_coqlib s;
       parse rem
 
     | ("-I"|"-include") :: d :: "-as" :: p :: rem -> deprecated "-I"; set_include d p; parse rem
diff --git a/lib/envars.ml b/lib/envars.ml
index dbd381bb2a..12cc9edfe4 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -107,12 +107,20 @@ let guess_coqlib fail =
 
 (** coqlib is now computed once during coqtop initialization *)
 
+(* Options for changing coqlib *)
+let coqlib_spec = ref false
+let coqlib = ref "(not initialized yet)"
+
+let set_user_coqlib path =
+  coqlib_spec := true;
+  coqlib := path
+
 let set_coqlib ~fail =
-  if not !Flags.coqlib_spec then
+  if not !coqlib_spec then
     let lib = if !Flags.boot then coqroot else guess_coqlib fail in
-    Flags.coqlib := lib
+    coqlib := lib
 
-let coqlib () = !Flags.coqlib
+let coqlib () = !coqlib
 
 let docdir () =
   (* This assumes implicitly that the suffix is non-trivial *)
diff --git a/lib/envars.mli b/lib/envars.mli
index 93d3cf9d0c..ebf86d0650 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -41,6 +41,9 @@ val configdir : unit -> string
 (** [set_coqlib] must be runned once before any access to [coqlib] *)
 val set_coqlib : fail:(string -> string) -> unit
 
+(** [set_user_coqlib path] sets the coqlib directory explicitedly. *)
+val set_user_coqlib : string -> unit
+
 (** [coqbin] is the name of the current executable. *)
 val coqbin : string
 
diff --git a/lib/flags.ml b/lib/flags.ml
index 54f25e209d..4d6c36f55d 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -121,10 +121,6 @@ let warn = ref true
 let make_warn flag = warn := flag;  ()
 let if_warn f x = if !warn then f x
 
-(* Options for changing coqlib *)
-let coqlib_spec = ref false
-let coqlib = ref "(not initialized yet)"
-
 (* Level of inlining during a functor application *)
 
 let default_inline_level = 100
diff --git a/lib/flags.mli b/lib/flags.mli
index 0faad1a541..398f22ab4f 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -118,10 +118,6 @@ val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b
 (** Temporarily extends the reference to a list *)
 val with_extra_values : 'c list ref -> 'c list -> ('a -> 'b) -> 'a -> 'b
 
-(** Options for specifying where coq librairies reside *)
-val coqlib_spec : bool ref
-val coqlib : string ref
-
 (** Level of inlining during a functor application *)
 val set_inline_level : int -> unit
 val get_inline_level : unit -> int
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 7db0b28908..ba88069be9 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -496,7 +496,7 @@ let rec parse = function
   | "-dumpgraphbox" :: f :: ll -> option_dump := Some (true, f); parse ll
   | "-exclude-dir" :: r :: ll -> System.exclude_directory r; parse ll
   | "-exclude-dir" :: [] -> usage ()
-  | "-coqlib" :: r :: ll -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll
+  | "-coqlib" :: r :: ll -> Envars.set_user_coqlib r; parse ll
   | "-coqlib" :: [] -> usage ()
   | "-suffix" :: s :: ll -> suffixe := s ; parse ll
   | "-suffix" :: [] -> usage ()
diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml
index 98a28bb2b6..1baaa8a45f 100644
--- a/toplevel/coqargs.ml
+++ b/toplevel/coqargs.ml
@@ -376,8 +376,7 @@ let parse_args arglist : coq_cmdopts * string list =
 
     (* Options with one arg *)
     |"-coqlib" ->
-      Flags.coqlib_spec := true;
-      Flags.coqlib := (next ());
+      Envars.set_user_coqlib (next ());
       oval
 
     |"-async-proofs" ->