From a81329a241ba18b8c8535576290a0ffa23739d27 Mon Sep 17 00:00:00 2001
From: notin
Date: Fri, 19 Dec 2008 15:30:49 +0000
Subject: 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
---
 ide/coq.ml      | 4 ++--
 ide/ideutils.ml | 5 +----
 2 files changed, 3 insertions(+), 6 deletions(-)

(limited to 'ide')

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
-- 
cgit v1.2.3