[config] Remove unused ML variables.

These are unused and not likely to come back.

3 files changed, 1 insertions, 31 deletions

diff --git a/config/coq_config.mli b/config/coq_config.mli
index 29065d3ef8..22d8c49fd1 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -23,26 +23,17 @@ val configdirsuffix : string (* config files relative to installation prefix *)
 val datadirsuffix : string   (* data files relative to installation prefix *)
 val docdirsuffix : string    (* doc directory relative to installation prefix *)
 
-val ocaml : string      (* names of ocaml binaries *)
 val ocamlfind : string
-val ocamllex : string
-
-val camlbin : string    (* base directory of OCaml binaries *)
-val camllib : string    (* for Dynlink *)
 
 val camlp5o : string    (* name of the camlp5o executable *)
 val camlp5bin : string  (* base directory for camlp5 binaries *)
 val camlp5lib : string  (* where is the library of camlp5 *)
 val camlp5compat : string (* compatibility argument to camlp5 *)
 
-val coqideincl : string (* arguments for building coqide (e.g. lablgtk) *)
-val cflags : string     (* arguments passed to gcc *)
 val caml_flags : string     (* arguments passed to ocamlc (ie. CAMLFLAGS) *)
 
-val best : string       (* byte/opt *)
 val arch : string       (* architecture *)
 val arch_is_win32 : bool
-val vmbyteflags : string list (* -custom/-dllib -lcoqrun *)
 
 val version : string    (* version number of Coq *)
 val caml_version : string    (* OCaml version used to compile Coq *)
@@ -52,8 +43,6 @@ val compile_date : string (* compile date *)
 val vo_magic_number : int
 val state_magic_number : int
 
-val core_src_dirs : string list
-val plugins_dirs : string list
 val all_src_dirs : string list
 
 val exec_extension : string (* "" under Unix, ".exe" under MS-windows *)
@@ -62,13 +51,9 @@ val browser : string
 (** default web browser to use, may be overridden by environment
     variable COQREMOTEBROWSER *)
 
-val has_coqide : string
 val gtk_platform : [`QUARTZ | `WIN32 | `X11]
 
 val has_natdynlink : bool
-val natdynlinkflag : string (* special cases of natdynlink (e.g. MacOS 10.5) *)
-
-val flambda_flags : string list
 
 val wwwcoq : string
 val wwwrefman : string
diff --git a/configure.ml b/configure.ml
index da6a6f8cbf..e3437a1d5b 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1187,13 +1187,11 @@ let write_configml f =
   let pr_i = pr "let %s = %d\n" in
   let pr_p s o = pr "let %s = %S\n" s
     (match o with Relative s -> s | Absolute s -> s) in
-  let pr_l  n l = pr "let %s = [%s]\n" n (String.concat ";" (List.map (fun s -> "\"" ^ s ^ "\"") l)) in
   let pr_li n l = pr "let %s = [%s]\n" n (String.concat ";" (List.map string_of_int l)) in
   pr "(* DO NOT EDIT THIS FILE: automatically generated by ../configure *)\n";
   pr "(* Exact command that generated this file: *)\n";
   pr "(* %s *)\n\n" (String.concat " " (Array.to_list Sys.argv));
   pr_b "local" !prefs.local;
-  pr "let vmbyteflags = ["; List.iter (pr "%S;") vmbyteflags; pr "]\n";
   pr_s "coqlib" coqlib;
   pr_s "configdir" configdir;
   pr_s "datadir" datadir;
@@ -1202,18 +1200,12 @@ let write_configml f =
   pr_p "configdirsuffix" configdirsuffix;
   pr_p "datadirsuffix" datadirsuffix;
   pr_p "docdirsuffix" docdirsuffix;
-  pr_s "ocaml" camlexec.top;
   pr_s "ocamlfind" camlexec.find;
-  pr_s "ocamllex" camlexec.lex;
-  pr_s "camlbin" camlbin;
-  pr_s "camllib" camllib;
   pr_s "camlp5o" camlp5o;
   pr_s "camlp5bin" camlp5bindir;
   pr_s "camlp5lib" camlp5libdir;
   pr_s "camlp5compat" camlp5compat;
-  pr_s "cflags" cflags;
   pr_s "caml_flags" caml_flags;
-  pr_s "best" best_compiler;
   pr_s "version" coq_version;
   pr_s "caml_version" caml_version;
   pr_li "caml_version_nums" caml_version_nums;
@@ -1222,12 +1214,8 @@ let write_configml f =
   pr_s "arch" arch;
   pr_b "arch_is_win32" arch_is_win32;
   pr_s "exec_extension" exe;
-  pr_s "coqideincl" !lablgtkincludes;
-  pr_s "has_coqide" coqide;
   pr "let gtk_platform = `%s\n" !idearchdef;
   pr_b "has_natdynlink" hasnatdynlink;
-  pr_s "natdynlinkflag" natdynlinkflag;
-  pr_l "flambda_flags" !prefs.flambda_flags;
   pr_i "vo_magic_number" vo_magic;
   pr_i "state_magic_number" state_magic;
   pr_s "browser" browser;
diff --git a/ide/coq.ml b/ide/coq.ml
index e948360191..88ffb4f0b7 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -42,14 +42,11 @@ let version () =
       "The Coq Proof Assistant, version %s (%s)\
        \nArchitecture %s running %s operating system\
        \nGtk version is %s\
-       \nThis is %s (%s is the best one for this architecture and OS)\
-       \n"
+       \nThis is %s \n"
       ver date
       Coq_config.arch Sys.os_type
       (let x,y,z = GMain.Main.version in Printf.sprintf "%d.%d.%d" x y z)
       (Filename.basename Sys.executable_name)
-      Coq_config.best
-
 
 (** * Initial checks by launching test coqtop processes *)