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

2 files changed, 3 insertions, 6 deletions

diff --git a/ide/coq.ml b/ide/coq.ml
index 809c502e7e..c605072515 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -58,7 +58,7 @@ let get_version_date () =
     then Coq_config.date
     else "<date not printable>" in
   try
-    let ch = open_in (Coq_config.coqtop^"/revision") in
+    let ch = open_in (Coq_config.coqsrc^"/revision") in
     let ver = input_line ch in
     let rev = input_line ch in
     (ver,rev)
@@ -88,7 +88,7 @@ let is_in_coq_lib dir =
   List.exists 
     (fun s -> 
       let fdir =
-        Filename.concat Coq_config.coqlib (Filename.concat "theories" s) in
+        Filename.concat (Envars.coqlib ()) (Filename.concat "theories" s) in
       prerr_endline (" Comparing to: "^fdir);
       if is_same_file fdir then (prerr_endline " YES";true)
       else (prerr_endline"NO";false))
diff --git a/ide/ideutils.ml b/ide/ideutils.ml
index 5295f273e5..be765922cd 100644
--- a/ide/ideutils.ml
+++ b/ide/ideutils.ml
@@ -33,10 +33,7 @@ let prerr_string s =
   if !debug then (prerr_string s;flush stderr)
 
 let lib_ide_file f =
-  let coqlib =
-    System.getenv_else "COQLIB"
-      (if Coq_config.local || !Flags.boot then Coq_config.coqtop
-       else Coq_config.coqlib) in
+  let coqlib = Envars.coqlib () in
   Filename.concat (Filename.concat coqlib "ide") f
   
 let get_insert input_buffer = input_buffer#get_iter_at_mark `INSERT