[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.

4 files changed, 14 insertions, 11 deletions

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