Configuration: always giving a value to configdir and datadir.

They were not used for looking for coqide files in the situation when
the effective installation path happens to be exactly the installation
path proposed by default, while relevant files were however (possibly)
installed in these directories.

4 files changed, 19 insertions, 23 deletions

diff --git a/config/coq_config.mli b/config/coq_config.mli
index c171bd355..59c96f73d 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -9,8 +9,8 @@
 val local : bool        (* local use (no installation) *)
 
 val coqlib : string option (* where the std library is installed *)
-val configdir : string option (* where configuration files are installed *)
-val datadir : string option (* where extra data files are installed *)
+val configdir : string  (* where configuration files are installed *)
+val datadir : string    (* where extra data files are installed *)
 val docdir : string     (* where the doc is installed *)
 
 val ocaml : string      (* names of ocaml binaries *)
diff --git a/configure.ml b/configure.ml
index 9902946e3..128751ea3 100644
--- a/configure.ml
+++ b/configure.ml
@@ -891,35 +891,33 @@ let relativize = function
   | Absolute path -> Relative (String.sub path 1 (String.length path - 1))
 
 let do_one_instdir (var,msg,uservalue,selfcontainedlayout,unixlayout) =
-  let dflt = if unix then use_suffix "/usr/local" unixlayout else use_suffix "C:/coq" selfcontainedlayout in
   let dir = match !uservalue, !Prefs.prefix with
     | Some d, _ -> d
     | _, Some p -> use_suffix p (if arch_is_win32 then selfcontainedlayout else relativize unixlayout)
     | _ ->
+      let dflt = if unix then use_suffix "/usr/local" unixlayout else use_suffix "C:/coq" selfcontainedlayout in
       let () = printf "Where should I install %s [%s]? " msg dflt in
       let line = read_line () in
       if line = "" then dflt else line
-  in (var,msg,dir,dir<>dflt)
+  in (var,msg,dir)
 
 let do_one_noinst (var,msg,_,_,_) =
-  if var="CONFIGDIR" || var="DATADIR" then (var,msg,coqtop^"/ide",true)
-  else (var,msg,coqtop^"/doc",false)
+  if var="CONFIGDIR" || var="DATADIR" then (var,msg,coqtop^"/ide")
+  else (var,msg,coqtop^"/doc")
 
 let install_dirs =
   let f = if !Prefs.local then do_one_noinst else do_one_instdir in
   List.map f install
 
-let select var = List.find (fun (v,_,_,_) -> v=var) install_dirs
+let select var = List.find (fun (v,_,_) -> v=var) install_dirs
 
-let coqlib = let (_,_,d,_) = select "COQLIBINSTALL" in d
+let coqlib = let (_,_,d) = select "COQLIBINSTALL" in d
 
-let docdir = let (_,_,d,_) = select "DOCDIR" in d
+let docdir = let (_,_,d) = select "DOCDIR" in d
 
-let configdir =
-  let (_,_,d,b) = select "CONFIGDIR" in if b then Some d else None
+let configdir = let (_,_,d) = select "CONFIGDIR" in d
 
-let datadir =
-  let (_,_,d,b) = select "DATADIR" in if b then Some d else None
+let datadir = let (_,_,d) = select "DATADIR" in d
 
 
 (** * OCaml runtime flags *)
@@ -986,7 +984,7 @@ let print_summary () =
   else
     (pr "  Paths for true installation:\n";
      List.iter
-       (fun (_,msg,dir,_) -> pr "  - %s will be copied in %s\n" msg dir)
+       (fun (_,msg,dir) -> pr "  - %s will be copied in %s\n" msg dir)
        install_dirs);
   pr "\n";
   pr "If anything is wrong above, please restart './configure'.\n\n";
@@ -1033,8 +1031,8 @@ let write_configml f =
   pr_b "local" !Prefs.local;
   pr "let vmbyteflags = ["; List.iter (pr "%S;") vmbyteflags; pr "]\n";
   pr_o "coqlib" (if !Prefs.local then None else Some coqlib);
-  pr_o "configdir" configdir;
-  pr_o "datadir" datadir;
+  pr_s "configdir" configdir;
+  pr_s "datadir" datadir;
   pr_s "docdir" docdir;
   pr_s "ocaml" camlexec.top;
   pr_s "ocamlfind" camlexec.find;
@@ -1119,8 +1117,8 @@ let write_makefile f =
   pr "VMBYTEFLAGS=%s\n" (String.concat " " vmbyteflags);
   pr "%s\n\n" !build_loadpath;
   pr "# Paths for true installation\n";
-  List.iter (fun (v,msg,_,_) -> pr "# %s: path for %s\n" v msg) install_dirs;
-  List.iter (fun (v,_,dir,_) -> pr "%s=%S\n" v dir) install_dirs;
+  List.iter (fun (v,msg,_) -> pr "# %s: path for %s\n" v msg) install_dirs;
+  List.iter (fun (v,_,dir) -> pr "%s=%S\n" v dir) install_dirs;
   pr "\n# Coq version\n";
   pr "VERSION=%s\n" coq_version;
   pr "VERSION4MACOS=%s\n\n" coq_macos_version;
diff --git a/ide/minilib.ml b/ide/minilib.ml
index 2c24e46f8..c9cef5639 100644
--- a/ide/minilib.ml
+++ b/ide/minilib.ml
@@ -54,12 +54,12 @@ let coqide_config_home () =
 let coqide_data_dirs () =
   coqify (Glib.get_user_data_dir ())
   :: List.map coqify (Glib.get_system_data_dirs ())
-  @ Option.List.cons Coq_config.datadir []
+  @ [Coq_config.datadir]
 
 let coqide_config_dirs () =
   coqide_config_home ()
   :: List.map coqify (Glib.get_system_config_dirs ())
-  @ Option.List.cons Coq_config.configdir []
+  @ [Coq_config.configdir]
 
 let is_prefix_of pre s =
   let i = ref 0 in
diff --git a/lib/envars.ml b/lib/envars.ml
index 0974368f6..989a18db9 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -23,8 +23,6 @@ let ( / ) a b =
 
 let coqify d = d / "coq"
 
-let opt2list = function None -> [] | Some x -> [x]
-
 let home ~warn =
   getenv_else "HOME" (fun () ->
     try (Sys.getenv "HOMEDRIVE")^(Sys.getenv "HOMEPATH") with Not_found ->
@@ -189,7 +187,7 @@ let xdg_data_dirs warn =
       | Not_found when String.equal Sys.os_type "Win32" -> [relative_base / "share"]
       | Not_found -> ["/usr/local/share/coq";"/usr/share/coq"]
   in
-  xdg_data_home warn :: sys_dirs @ opt2list Coq_config.datadir
+  xdg_data_home warn :: sys_dirs @ [Coq_config.datadir]
 
 let xdg_dirs ~warn =
   List.filter Sys.file_exists (xdg_data_dirs warn)