All invocations to ocaml compilers go through ocamlfind

Nothing is done for camlp4
There is an issue with computing camlbindir

4 files changed, 15 insertions, 37 deletions

diff --git a/lib/envars.ml b/lib/envars.ml
index ac0b6f722e..1cb140b94d 100644
--- a/lib/envars.ml
+++ b/lib/envars.ml
@@ -156,36 +156,23 @@ let coqpath =
 
 let exe s = s ^ Coq_config.exec_extension
 
-let guess_camlbin () = which (user_path ()) (exe "ocamlc")
+let guess_ocamlfind () = fst (which (user_path ()) (exe "ocamlfind"))
 
-let camlbin () =
-  if !Flags.camlbin_spec then !Flags.camlbin else
-    if !Flags.boot then Coq_config.camlbin else
-      try guess_camlbin () with Not_found -> Coq_config.camlbin
-
-let ocamlc () = camlbin () / Coq_config.ocamlc
-
-let ocamlopt () = camlbin () / Coq_config.ocamlopt
-
-let camllib () =
-  if !Flags.boot then
-    Coq_config.camllib
-  else
-    let _, res = CUnix.run_command (ocamlc () ^ " -where") in
-    String.strip res
+let ocamlfind () =
+  if !Flags.ocamlfind_spec then !Flags.ocamlfind else
+    if !Flags.boot then Coq_config.ocamlfind else
+      try guess_ocamlfind () with Not_found -> Coq_config.ocamlfind
 
 (** {2 Camlp4 paths} *)
 
-let guess_camlp4bin () = which (user_path ()) (exe Coq_config.camlp4)
+let guess_camlp4bin () = snd (which (user_path ()) (exe Coq_config.camlp4))
 
 let camlp4bin () =
   if !Flags.camlp4bin_spec then !Flags.camlp4bin else
     if !Flags.boot then Coq_config.camlp4bin else
       try guess_camlp4bin ()
       with Not_found ->
-        let cb = camlbin () in
-        if Sys.file_exists (cb / exe Coq_config.camlp4) then cb
-        else Coq_config.camlp4bin
+        Coq_config.camlp4bin
 
 let camlp4 () = camlp4bin () / exe Coq_config.camlp4
 
@@ -193,7 +180,7 @@ let camlp4lib () =
   if !Flags.boot then
     Coq_config.camlp4lib
   else
-    let ex, res = CUnix.run_command (camlp4 () ^ " -where") in
+    let ex, res = CUnix.run_command (ocamlfind () ^ " query " ^ Coq_config.camlp4) in
     match ex with
       | Unix.WEXITED 0 -> String.strip res
       | _ -> "/dev/null"
diff --git a/lib/envars.mli b/lib/envars.mli
index b62b9f28a9..7c20c035a5 100644
--- a/lib/envars.mli
+++ b/lib/envars.mli
@@ -47,17 +47,8 @@ val coqroot : string
     the order it gets added to the search path. *)
 val coqpath : string list
 
-(** [camlbin ()] is the path to the ocaml binaries. *)
-val camlbin : unit -> string
-
-(** [camllib ()] is the path to the ocaml standard library. *)
-val camllib : unit -> string
-
-(** [ocamlc ()] is the ocaml bytecode compiler that compiled this Coq. *)
-val ocamlc   : unit -> string
-
-(** [ocamlc ()] is the ocaml native compiler that compiled this Coq. *)
-val ocamlopt : unit -> string
+(** [camlbin ()] is the path to the ocamlfind binary. *)
+val ocamlfind : unit -> string
 
 (** [camlp4bin ()] is the path to the camlp4 binary. *)
 val camlp4bin : unit -> string
diff --git a/lib/flags.ml b/lib/flags.ml
index 009caa9dee..fe580b7fff 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -193,9 +193,9 @@ let is_standard_doc_url url =
 let coqlib_spec = ref false
 let coqlib = ref "(not initialized yet)"
 
-(* Options for changing camlbin (used by coqmktop) *)
-let camlbin_spec = ref false
-let camlbin = ref Coq_config.camlbin
+(* Options for changing ocamlfind (used by coqmktop) *)
+let ocamlfind_spec = ref false
+let ocamlfind = ref Coq_config.camlbin
 
 (* Options for changing camlp4bin (used by coqmktop) *)
 let camlp4bin_spec = ref false
diff --git a/lib/flags.mli b/lib/flags.mli
index 544e2a72ae..bdb8159add 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -120,8 +120,8 @@ val coqlib_spec : bool ref
 val coqlib : string ref
 
 (** Options for specifying where OCaml binaries reside *)
-val camlbin_spec : bool ref
-val camlbin : string ref
+val ocamlfind_spec : bool ref
+val ocamlfind : string ref
 val camlp4bin_spec : bool ref
 val camlp4bin : string ref