Nettoyage des variables Coq et amélioration de coqmktop. Les

principaux changements sont:
  - coqtop (et coqc) maintenant insensible aux variables
    d'environnement COQTOP, COQBIN et COQLIB; le chemin vers les
    librairies Coq peut être spécifié par l'option -coqlib
  - coqmktop prend 4 nouvelles options: -boot, -coqlib, -camlbin et
    -camlp4bin; en mode boot, coqmktop se réfère à Coq_config pour les
    chemins des exécutables OCaml; en dehors du mode boot, coqmktop
    cherche les exécutables OCaml dans PATH
  - installation des *.cmxs *.o et *.a en plus des *.cm[ioxa]; ceux-ci
    étant installé en copiant l'architecture des sources (ie lib.cmxa
    est installé dans COQLIB/lib/lib.cmxa)
  - coq_makefile prend maintenant 3 paramètres sous forme de variables
    d'environnement: COQBIN pour dire où trouver les exécutables Coq,
    CAMLBIN et CAMLP4BIN pour les exécutables OCaml et Camlp4/5; les
    chemins vers les librairies sont déduits en utilisant -where

Le tout a testé avec Ssreflect (cf coq-contribs) en essayant de
simuler les conditions de la vie réelle (Ocaml pas dans le PATH,
installation binaire relocalisée, ...). 




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11707 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 5 insertions, 5 deletions

diff --git a/contrib/dp/dp_gappa.ml b/contrib/dp/dp_gappa.ml
index f77f1a5c48..9c035aa855 100644
--- a/contrib/dp/dp_gappa.ml
+++ b/contrib/dp/dp_gappa.ml
@@ -153,7 +153,7 @@ let call_gappa hl p =
   let gappa_out2 = temp_file "gappa2" in
   patch_gappa_proof gappa_out gappa_out2;
   remove_file gappa_out;
-  let cmd = sprintf "%s/coqc %s" Coq_config.bindir gappa_out2 in
+  let cmd = (Filename.concat (Envars.coqbin ()) "coqc") ^ " " ^ gappa_out2 in
   let out = Sys.command cmd in
   if out <> 0 then raise GappaProofFailed;
   let gappa_out3 = temp_file "gappa3" in
@@ -164,7 +164,7 @@ let call_gappa hl p =
     (Filename.chop_suffix gappa_out2 ".v") gappa2;
   close_out c;
   let lambda = temp_file "gappa_lambda" in
-  let cmd = sprintf "%s/coqc %s > %s" Coq_config.bindir gappa_out3 lambda in
+  let cmd = (Filename.concat (Envars.coqbin ()) "coqc") ^ " " ^ gappa_out3 ^ " > " ^ lambda in
   let out = Sys.command cmd in
   if out <> 0 then raise GappaProofFailed;
   remove_file gappa_out2; remove_file gappa_out3;
diff --git a/contrib/interface/parse.ml b/contrib/interface/parse.ml
index b551b143c2..5de6060f05 100644
--- a/contrib/interface/parse.ml
+++ b/contrib/interface/parse.ml
@@ -370,7 +370,7 @@ Libobject.relax true;
 (let coqdir = 
    try Sys.getenv "COQDIR"
    with Not_found -> 
-     let coqdir = Coq_config.coqlib in
+     let coqdir = Envars.coqlib () in
        if Sys.file_exists coqdir then
 	 coqdir
        else
diff --git a/contrib/micromega/coq_micromega.ml b/contrib/micromega/coq_micromega.ml
index 890671ab5d..e9a8a0e3b1 100644
--- a/contrib/micromega/coq_micromega.ml
+++ b/contrib/micromega/coq_micromega.ml
@@ -1294,7 +1294,7 @@ let call_csdpcert provername poly =
   output_value ch_to (provername,poly : provername * micromega_polys);
   close_out ch_to;
   let cmdname =
-    List.fold_left Filename.concat Coq_config.coqlib
+    List.fold_left Filename.concat (Envars.coqlib ())
       ["contrib"; "micromega"; "csdpcert" ^ Coq_config.exec_extension] in
   let c = Sys.command (cmdname ^" "^ tmp_to ^" "^ tmp_from) in
   (try Sys.remove tmp_to with _ -> ());
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml
index 3c4b01f5bb..4ee97813bd 100644
--- a/contrib/xml/xmlcommand.ml
+++ b/contrib/xml/xmlcommand.ml
@@ -691,7 +691,7 @@ let _ =
        end ;
        Option.iter 
 	(fun fn ->
-	  let coqdoc = Coq_config.bindir^"/coqdoc" in
+	  let coqdoc = Filename.concat (Envars.coqbin ()) ("coqdoc" ^ Coq_config.exec_extension) in
 	  let options = " --html -s --body-only --no-index --latin1 --raw-comments" in
 	  let dir = Option.get xml_library_root in
           let command cmd =