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

26 files changed, 303 insertions, 181 deletions

diff --git a/Makefile.build b/Makefile.build
index 5388b20b0..4e3dd1c5e 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -179,12 +179,12 @@ initplugins: $(INITPLUGINSOPT) $(INITPLUGINS)
 
 $(COQTOPOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'	
-	$(HIDE)$(COQMKTOP) -opt $(OPTFLAGS) -o $@
+	$(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) -o $@
 	$(STRIP) $@
 
 $(COQTOPBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN)
 	$(SHOW)'COQMKTOP -o $@'	
-	$(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@
+	$(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@
 
 $(COQTOPEXE): $(ORDER_ONLY_SEP) $(BESTCOQTOP)
 	cd bin; ln -sf coqtop.$(BEST)$(EXE) coqtop$(EXE)
@@ -196,12 +196,12 @@ CHKOPTFLAGS:=$(CHKLIBS) $(CAMLDEBUGOPT) $(CAMLTIMEPROF) $(USERFLAGS)
 
 $(CHICKENOPT): checker/check.cmxa checker/main.ml
 	$(SHOW)'OCAMLOPT -o $@'
-	$(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -o $@ unix.cmxa gramlib.cmxa $^
+	$(HIDE)$(OCAMLOPT) $(CHKOPTFLAGS) -o $@ str.cmxa unix.cmxa gramlib.cmxa $^
 	$(STRIP) $@
 
 $(CHICKENBYTE): checker/check.cma checker/main.ml
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -o $@ unix.cma gramlib.cma $^
+	$(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^
 
 $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN)
 	cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE)
@@ -210,11 +210,13 @@ $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN)
 
 $(COQMKTOPBYTE): $(COQMKTOPCMO)
 	$(SHOW)'OCAMLC -o $@'	
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma $^ $(OSDEPLIBS)
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma\
+          $^ $(OSDEPLIBS)
 
 $(COQMKTOPOPT): $(COQMKTOPCMX)
 	$(SHOW)'OCAMLOPT -o $@'	
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa $^ $(OSDEPLIBS)
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa gramlib.cmxa\
+          $^ $(OSDEPLIBS)
 	$(STRIP) $@
 
 $(COQMKTOP): $(ORDER_ONLY_SEP) $(BESTCOQMKTOP)
@@ -231,11 +233,11 @@ scripts/tolink.ml: Makefile.build Makefile.common
 
 $(COQCBYTE): $(COQCCMO) $(COQTOPBYTE) $(BESTCOQTOP)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $(COQCCMO) $(OSDEPLIBS)
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $(COQCCMO) $(OSDEPLIBS)
 
 $(COQCOPT): $(COQCCMX) $(COQTOPOPT) $(BESTCOQTOP)
 	$(SHOW)'OCAMLOPT -o $@'
-	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ unix.cmxa $(COQCCMX) $(OSDEPLIBS)
+	$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -o $@ str.cmxa unix.cmxa gramlib.cmxa $(COQCCMX) $(OSDEPLIBS)
 	$(STRIP) $@
 
 $(COQC): $(ORDER_ONLY_SEP) $(BESTCOQC)
@@ -399,12 +401,12 @@ coqide-files: $(IDEFILES)
 
 $(COQIDEOPT): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) ide/ide.cmxa
 	$(SHOW)'COQMKTOP -o $@'	
-	$(HIDE)$(COQMKTOP) -ide -opt $(OPTFLAGS) -o $@
+	$(HIDE)$(COQMKTOP) -boot -ide -opt $(OPTFLAGS) -o $@
 	$(STRIP) $@
 
 $(COQIDEBYTE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) ide/ide.cma
 	$(SHOW)'COQMKTOP -o $@'	
-	$(HIDE)$(COQMKTOP) -g -ide -top $(BYTEFLAGS) -o $@
+	$(HIDE)$(COQMKTOP) -boot -g -ide -top $(BYTEFLAGS) -o $@
 
 $(COQIDE):
 	cd bin; ln -sf coqide.$(HASCOQIDE)$(EXE) coqide$(EXE)
@@ -466,21 +468,21 @@ pcoq-binaries:: $(COQINTERFACE)
 
 bin/coq-interface$(EXE): $(COQMKTOP) $(LINKCMO) $(LIBCOQRUN) $(INTERFACE)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(COQMKTOP) -top $(BYTEFLAGS) -o $@ $(INTERFACE)
+	$(HIDE)$(COQMKTOP) -boot -top $(BYTEFLAGS) -o $@ $(INTERFACE)
 
 bin/coq-interface.opt$(EXE): $(COQMKTOP) $(LINKCMX) $(LIBCOQRUN) $(INTERFACECMX)
 	$(SHOW)'COQMKTOP -o $@'
-	$(HIDE)$(COQMKTOP) -opt $(OPTFLAGS) -o $@ $(INTERFACECMX)
+	$(HIDE)$(COQMKTOP) -boot -opt $(OPTFLAGS) -o $@ $(INTERFACECMX)
 
 bin/coq-parser$(EXE):$(LIBCOQRUN) $(PARSERCMO)
 	$(SHOW)'OCAMLC -o $@'
 	$(HIDE)$(OCAMLC) $(COQRUNBYTEFLAGS) -linkall $(BYTEFLAGS) -o $@ \
-	  dynlink.cma nums.cma $(LIBCOQRUN) $(CMA) $(PARSERCMO)
+	  dynlink.cma str.cma nums.cma $(LIBCOQRUN) $(CMA) $(PARSERCMO)
 
 bin/coq-parser.opt$(EXE): $(LIBCOQRUN) $(PARSERCMX)
 	$(SHOW)'OCAMLOPT -o $@'
 	$(HIDE)$(OCAMLOPT) -linkall $(OPTFLAGS) -o $@ \
-	  $(LIBCOQRUN) $(DYNLINKCMXA) nums.cmxa $(CMXA) $(PARSERCMX)
+	  $(LIBCOQRUN) $(DYNLINKCMXA) str.cmxa nums.cmxa $(CMXA) $(PARSERCMX)
 
 pcoq-files:: $(INTERFACEVO) $(INTERFACERC)
 
@@ -595,7 +597,7 @@ tools:: $(TOOLS) $(DEBUGPRINTERS)
 
 $(COQDEP): $(COQDEPCMO)
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ unix.cma $^ $(OSDEPLIBS)
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma gramlib.cma $^ $(OSDEPLIBS)
 
 $(GALLINA): $(GALLINACMO)
 	$(SHOW)'OCAMLC -o $@'
@@ -667,11 +669,12 @@ install-library:
 	$(MKDIR) $(FULLCOQLIB)/states
 	$(INSTALLLIB) states/*.coq $(FULLCOQLIB)/states
 	$(MKDIR) $(FULLCOQLIB)/user-contrib
-	$(INSTALLLIB) $(LINKCMO) $(GRAMMARCMA) $(FULLCOQLIB)
+	cp --parents $(LINKCMO) $(GRAMMARCMA) $(FULLCOQLIB)
 ifeq ($(BEST),opt)
-	$(INSTALLLIB) $(LINKCMX) $(FULLCOQLIB)
+	cp --parents $(LINKCMX) $(FULLCOQLIB)
 endif
-	find . $(FIND_VCS_CLAUSE) $(PRUNE_CHECKER) -name \*.cmi -exec $(INSTALLLIB) {} $(FULLCOQLIB) \;
+	find . $(FIND_VCS_CLAUSE) \( -name \*.o -o -name \*.a -o -name \*.cmxs \) -exec cp --parents {} $(FULLCOQLIB) \;
+	find . $(FIND_VCS_CLAUSE) -name \*.cmi -exec cp --parents {} $(FULLCOQLIB) \;
 # csdpcert is not meant to be directly called by the user; we install
 # it with libraries
 	-$(MKDIR) -p $(FULLCOQLIB)/contrib/micromega
diff --git a/Makefile.common b/Makefile.common
index 63740d086..c2f3e305b 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -1,3 +1,4 @@
+
 #######################################################################
 #  v      #   The Coq Proof Assistant  /  The Coq Development Team    #
 # <O___,, #        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              #
@@ -130,7 +131,7 @@ CONFIG:=\
 LIBREP:=\
   lib/pp_control.cmo lib/pp.cmo lib/compat.cmo lib/flags.cmo \
   lib/util.cmo lib/bigint.cmo lib/hashcons.cmo lib/dyn.cmo lib/system.cmo \
-  lib/bstack.cmo lib/edit.cmo lib/gset.cmo lib/gmap.cmo \
+  lib/envars.cmo lib/bstack.cmo lib/edit.cmo lib/gset.cmo lib/gmap.cmo \
   lib/tlm.cmo lib/gmapl.cmo lib/profile.cmo lib/explore.cmo \
   lib/predicate.cmo lib/rtree.cmo lib/heap.cmo lib/option.cmo
 # Rem: Cygwin already uses variable LIB 
@@ -391,11 +392,14 @@ COQIDECMO:=ide/utils/okey.cmo ide/utils/config_file.cmo \
 
 COQIDECMX:=$(COQIDECMO:.cmo=.cmx)
 
-COQMKTOPCMO:=$(CONFIG) scripts/tolink.cmo scripts/coqmktop.cmo 
+COQENVCMO:=$(CONFIG) lib/pp_control.cmo lib/pp.cmo  lib/compat.cmo lib/flags.cmo \
+	lib/util.cmo lib/system.cmo lib/envars.cmo
+
+COQMKTOPCMO:=$(COQENVCMO) scripts/tolink.cmo scripts/coqmktop.cmo 
+COQMKTOPCMX:=$(COQMKTOPCMO:.cmo=.cmx)
 
-COQMKTOPCMX:=config/coq_config.cmx scripts/tolink.cmx scripts/coqmktop.cmx 
-COQCCMO:=$(CONFIG) toplevel/usage.cmo lib/pp_control.cmo lib/pp.cmo scripts/coqc.cmo
-COQCCMX:=config/coq_config.cmx toplevel/usage.cmx lib/pp_control.cmx lib/pp.cmx scripts/coqc.cmx
+COQCCMO:=$(COQENVCMO) toplevel/usage.cmo scripts/coqc.cmo
+COQCCMX:=$(COQCCMO:.cmo=.cmx)
 
 INTERFACE:=\
   contrib/interface/vtp.cmo contrib/interface/xlate.cmo \
@@ -433,7 +437,7 @@ CSDPCERTCMX:= $(CSDPCERTCMO:.cmo=.cmx)
 
 DEBUGPRINTERS:=dev/top_printers.cmo dev/vm_printers.cmo dev/printers.cma
 
-COQDEPCMO:=config/coq_config.cmo tools/coqdep_lexer.cmo tools/coqdep.cmo
+COQDEPCMO:=$(COQENVCMO) tools/coqdep_lexer.cmo tools/coqdep.cmo
 GALLINACMO:=tools/gallina_lexer.cmo tools/gallina.cmo
 COQDOCCMO:=$(CONFIG) tools/coqdoc/cdglobals.cmo tools/coqdoc/alpha.cmo \
 	tools/coqdoc/index.cmo tools/coqdoc/output.cmo \
@@ -446,7 +450,7 @@ MCHECKER:=\
   config/coq_config.cmo \
   lib/pp_control.cmo lib/pp.cmo lib/compat.cmo \
   lib/flags.cmo lib/util.cmo lib/option.cmo lib/hashcons.cmo \
-  lib/system.cmo \
+  lib/system.cmo lib/envars.cmo \
   lib/predicate.cmo lib/rtree.cmo \
   kernel/names.cmo kernel/univ.cmo \
   kernel/esubst.cmo checker/term.cmo \
diff --git a/Makefile.doc b/Makefile.doc
index 10550da3a..9f98cc2b5 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -153,12 +153,12 @@ doc/faq/html/index.html: doc/faq/FAQ.v.html
 doc/stdlib/index-body.html: | $(COQDOC) $(THEORIESVO)
 	- rm -rf doc/stdlib/html
 	$(MKDIR) doc/stdlib/html
-	$(COQDOC) -q -d doc/stdlib/html --multi-index --html \
+	$(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html \
 	  -R theories Coq $(THEORIESVO:.vo=.v)
 	mv doc/stdlib/html/index.html doc/stdlib/index-body.html
 
 doc/stdlib/index-list.html: doc/stdlib/index-list.html.template
-	COQTOP=$(COQSRC) ./doc/stdlib/make-library-index doc/stdlib/index-list.html
+	./doc/stdlib/make-library-index doc/stdlib/index-list.html
 
 doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.html doc/stdlib/index-trailer.html
 	cat doc/stdlib/index-list.html > $@
@@ -168,7 +168,7 @@ doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.htm
 ### Standard library (light version, full version is definitely too big)
 
 doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO)
-	$(COQSRC)/$(COQDOC) -q --gallina --body-only --latex --stdout \
+	$(COQDOC) -q -boot --gallina --body-only --latex --stdout \
             -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@
 
 doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex
diff --git a/checker/checker.ml b/checker/checker.ml
index 1ed094cf2..9c1802cab 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -43,7 +43,7 @@ let (/) = Filename.concat
 
 let get_version_date () =
   try
-    let ch = open_in (Coq_config.coqlib^"/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)
@@ -108,13 +108,9 @@ let set_rec_include d p =
   check_coq_overwriting p;
   push_rec_include(d,p)
 
-(* Initializes the LoadPath according to COQLIB and Coq_config *)
+(* Initializes the LoadPath *)
 let init_load_path () =
-  let coqlib =
-    (* variable COQLIB overrides the default library *)
-    getenv_else "COQLIB"
-      (if Coq_config.local || !Flags.boot then Coq_config.coqtop
-	else Coq_config.coqlib) in
+  let coqlib = Envars.coqlib () in
   let user_contrib = coqlib/"user-contrib" in
   let contrib = coqlib/"contrib" in
   (* first user-contrib *)
@@ -323,7 +319,7 @@ let parse_args() =
     | "-debug" :: rem -> set_debug (); parse rem
 
     | "-where" :: _ ->
-        print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0
+        print_endline (Envars.coqlib ()); exit 0
 
     | ("-?"|"-h"|"-H"|"-help"|"--help") :: _ -> usage ()
 
diff --git a/config/coq_config.mli b/config/coq_config.mli
index e5a32708d..1eff9c38d 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -10,15 +10,14 @@
 
 val local : bool        (* local use (no installation) *)
 
-val bindir : string     (* where the binaries are installed *)
 val coqlib : string     (* where the std library is installed *)
+val coqsrc : string     (* where are the sources *)
 
-val coqtop : string     (* where are the sources *)
-
-val camldir : string    (* base directory of OCaml binaries *)
+val camlbin : string    (* base directory of OCaml binaries *)
 val camllib : string    (* for Dynlink *)
 
 val camlp4 : string     (* exact name of camlp4: either "camlp4" ou "camlp5" *)
+val camlp4bin : string  (* base directory for Camlp4/5 binaries *)
 val camlp4lib : string  (* where is the library of Camlp4 *)
 
 val best : string       (* byte/opt *)
diff --git a/configure b/configure
index b9e6f9ea8..72c1ba8be 100755
--- a/configure
+++ b/configure
@@ -862,6 +862,7 @@ case $ARCH in
     win32)
 	ESCCOQTOP=`echo $COQTOP |sed -e 's|\\\|\\\\\\\|g'`
 	ESCBINDIR=`echo $BINDIR |sed -e 's|\\\|\\\\\\\|g'`
+	ESCSRCDIR=`echo $COQSRC |sed -e 's|\\\|\\\\\\\|g'`
 	ESCLIBDIR=`echo $LIBDIR |sed -e 's|\\\|\\\\\\\|g'`
 	ESCCAMLDIR=`echo $CAMLBIN |sed -e 's|\\\|\\\\\\\|g'`
 	ESCCAMLLIB=`echo $CAMLLIB |sed -e 's|\\\|\\\\\\\|g'`
@@ -876,6 +877,7 @@ case $ARCH in
     *)
         ESCCOQTOP="$COQTOP"
 	ESCBINDIR="$BINDIR"
+	ESCSRCDIR="$COQSRC"
 	ESCLIBDIR="$LIBDIR"
 	ESCCAMLDIR="$CAMLBIN"
 	ESCCAMLLIB="$CAMLLIB"
@@ -896,12 +898,12 @@ cat << END_OF_COQ_CONFIG > $mlconfig_file
 
 let local = $local
 let coqrunbyteflags = "$COQRUNBYTEFLAGS"
-let bindir = try Sys.getenv "COQBIN" with Not_found -> "$ESCBINDIR"
-let coqlib = try Sys.getenv "COQLIB" with Not_found -> "$ESCLIBDIR"
-let coqtop = try Sys.getenv "COQTOP" with Not_found -> "$ESCCOQTOP"
-let camldir = "$ESCCAMLDIR"
+let coqlib = "$ESCLIBDIR"
+let coqsrc = "$ESCSRCDIR"
+let camlbin = "$ESCCAMLDIR"
 let camllib = "$ESCCAMLLIB"
 let camlp4 = "$CAMLP4"
+let camlp4bin = "$ESCCAMLP4BIN"
 let camlp4lib = "$ESCCAMLP4LIB"
 let best = "$best_compiler"
 let arch = "$ARCH"
diff --git a/contrib/dp/dp_gappa.ml b/contrib/dp/dp_gappa.ml
index f77f1a5c4..9c035aa85 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 b551b143c..5de6060f0 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 890671ab5..e9a8a0e3b 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 3c4b01f5b..4ee97813b 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 =
diff --git a/doc/stdlib/make-library-files b/doc/stdlib/make-library-files
index add14a13b..9516a19ff 100755
--- a/doc/stdlib/make-library-files
+++ b/doc/stdlib/make-library-files
@@ -1,6 +1,6 @@
 #!/bin/sh
 
-# Needs COQTOP and GALLINA set
+# Needs COQSRC and GALLINA set
 
 # On garde la liste de tous les *.v avec dates dans library.files.ls
 # Si elle a change depuis la derniere fois ou library.files n'existe pas
@@ -13,12 +13,12 @@
 LIBDIRS="Arith NArith ZArith Reals Logic Bool Lists Relations Sets Sorting Wellfounded Setoids Program Classes"
 
 rm -f library.files.ls.tmp
-(cd $COQTOP/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp
+(cd $COQSRC/theories; find $LIBDIR -name "*.v" -ls) > library.files.ls.tmp
 if ! test -e library.files || ! cmp library.files.ls library.files.ls.tmp; then
   mv -f library.files.ls.tmp library.files.ls
   rm -f library.files; touch library.files
   ABSOLUTE=`pwd`/library.files
-  cd $COQTOP/theories
+  cd $COQSRC/theories
   echo $LIBDIRS
   for rep in $LIBDIRS ; do
     (cd $rep
diff --git a/ide/coq.ml b/ide/coq.ml
index 809c502e7..c60507251 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 5295f273e..be765922c 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
diff --git a/lib/envars.ml b/lib/envars.ml
new file mode 100644
index 000000000..82e0d3162
--- /dev/null
+++ b/lib/envars.ml
@@ -0,0 +1,83 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* This file gathers environment variables needed by Coq to run (such
+   as coqlib) *)
+
+let coqbin () = 
+  if !Flags.boot || Coq_config.local
+  then Filename.concat Coq_config.coqsrc "bin"
+  else Filename.dirname Sys.executable_name
+
+let guess_coqlib () = 
+  let file = "states/initial.coq" in
+    if Sys.file_exists (Filename.concat Coq_config.coqlib file) 
+    then Coq_config.coqlib
+    else 
+      let prefix = Filename.dirname (Filename.dirname Sys.executable_name) in
+      let coqlib = if Coq_config.local then prefix else 
+	List.fold_left Filename.concat prefix ["lib";"coq"] in
+	if Sys.file_exists (Filename.concat coqlib file) then coqlib else
+	  Util.error "cannot guess a path for Coq libraries; please use -coqlib option"
+	  
+let coqlib () = 
+  if !Flags.coqlib_spec then !Flags.coqlib else
+    (if !Flags.boot then Coq_config.coqsrc else guess_coqlib ())
+
+let path_to_list p =
+  let sep = Str.regexp_string (if Sys.os_type = "Win32" then ";" else ":") in
+    Str.split sep p 
+
+let rec which l f =
+  match l with
+    | [] -> raise Not_found
+    | p :: tl -> 
+	if Sys.file_exists (Filename.concat p f) 
+	then p 
+	else which tl f
+ 
+let guess_camlbin () = 
+  let path = try Sys.getenv "PATH" with _ -> raise Not_found in 
+  let lpath = path_to_list path in
+    which lpath "ocamlc"
+
+let guess_camlp4bin () = 
+  let path = try Sys.getenv "PATH" with _ -> raise Not_found in 
+  let lpath = path_to_list path in
+    which lpath Coq_config.camlp4
+
+let camlbin () = 
+  if !Flags.camlbin_spec then !Flags.camlbin else
+    if !Flags.boot then Coq_config.camlbin else
+      try guess_camlbin () with _ -> Coq_config.camlbin
+
+let camllib () = 
+  if !Flags.boot
+  then Coq_config.camllib
+  else 
+    let camlbin = camlbin () in 
+    let com = (Filename.concat camlbin "ocamlc") ^ " -where" in
+    let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in
+      res
+
+(* TODO : essayer aussi camlbin *)
+let camlp4bin () = 
+  if !Flags.camlp4bin_spec then !Flags.camlp4bin else
+    if !Flags.boot then Coq_config.camlp4bin else
+      try guess_camlp4bin () with _ -> Coq_config.camlp4bin
+
+let camlp4lib () = 
+  if !Flags.boot
+  then Coq_config.camlp4lib
+  else 
+    let camlp4bin = camlp4bin () in 
+    let com = (Filename.concat camlp4bin Coq_config.camlp4) ^ " -where" in
+    let _,res = System.run_command (fun x -> x) (fun _ -> ()) com in
+      res
+
+    
diff --git a/lib/envars.mli b/lib/envars.mli
new file mode 100644
index 000000000..62d0cb61d
--- /dev/null
+++ b/lib/envars.mli
@@ -0,0 +1,15 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+val coqlib : unit -> string
+val coqbin : unit -> string
+
+val camlbin : unit -> string
+val camlp4bin : unit -> string
+val camllib : unit -> string
+val camlp4lib : unit -> string
diff --git a/lib/flags.ml b/lib/flags.ml
index f4b36c6c3..c3033c4b5 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -104,3 +104,16 @@ let browser_cmd_fmt =
   Sys.getenv coq_netscape_remote_var
  with
   Not_found -> Coq_config.browser
+
+(* Options for changing coqlib *)
+let coqlib_spec = ref false
+let coqlib = ref Coq_config.coqlib
+
+(* Options for changing camlbin (used by coqmktop) *)
+let camlbin_spec = ref false
+let camlbin = ref Coq_config.camlbin
+
+(* Options for changing camlp4bin (used by coqmktop) *)
+let camlp4bin_spec = ref false
+let camlp4bin = ref Coq_config.camlp4bin
+
diff --git a/lib/flags.mli b/lib/flags.mli
index db472cccb..f0e4103f6 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -68,3 +68,13 @@ val browser_cmd_fmt : string
  
 (* Substitute %s in the first chain by the second chain *)
 val subst_command_placeholder : string -> string -> string
+
+(* Options for specifying where coq librairies reside *)
+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 camlp4bin_spec : bool ref
+val camlp4bin : string ref
diff --git a/scripts/coqc.ml b/scripts/coqc.ml
index bee9e7b32..f2cf2025d 100644
--- a/scripts/coqc.ml
+++ b/scripts/coqc.ml
@@ -24,17 +24,9 @@
 
 let environment = Unix.environment ()
 
-let bindir = ref Coq_config.bindir
 let binary = ref ("coqtop." ^ Coq_config.best)
 let image = ref ""
 
-(* the $COQBIN environment variable has priority over the Coq_config value *)
-let _ = 
-  try 
-    let c = Sys.getenv "COQBIN" in
-    if c <> "" then bindir := c
-  with Not_found -> ()
-
 (* coqc options *)
 
 let specification = ref false
@@ -116,12 +108,8 @@ let parse_args () =
     | ("-verbose" | "--verbose") :: rem -> 
 	verbose := true ; parse (cfiles,args) rem
     | "-boot" :: rem ->
-	bindir:= Filename.concat Coq_config.coqtop "bin";
+	Flags.boot := true;
 	parse (cfiles, "-boot"::args) rem
-    | "-bindir" :: d :: rem ->
-	bindir := d ; parse (cfiles,args) rem
-    | "-bindir" :: []       ->
-	usage ()
     | "-byte" :: rem ->
 	binary := "coqtop.byte"; parse (cfiles,args) rem
     | "-opt" :: rem ->
@@ -141,7 +129,7 @@ let parse_args () =
     | ("-I"|"-include"|"-outputstate"
       |"-inputstate"|"-is"|"-load-vernac-source"|"-l"|"-load-vernac-object"
       |"-load-ml-source"|"-require"|"-load-ml-object"|"-user"
-      |"-init-file" | "-dump-glob" as o) :: rem ->
+      |"-init-file" | "-dump-glob" | "-coqlib" as o) :: rem ->
 	begin
 	  match rem with
 	    | s :: rem' -> parse (cfiles,s::o::args) rem'
@@ -158,12 +146,11 @@ let parse_args () =
       |"-unboxed-values"|"-unboxed-definitions"|"-draw-vm-instr"
       |"-no-glob"|"-noglob" as o) :: rem ->
 	parse (cfiles,o::args) rem
-
-    | "-where" :: _ -> 
-	let coqlib = 
-	  try Sys.getenv "COQLIB" with Not_found -> Coq_config.coqlib 
-	in
-	  print_endline coqlib; exit 0
+	    
+    | ("-where") :: _ -> 
+	(try print_endline (Envars.coqlib ())
+	 with Util.UserError(_,pps) -> Pp.msgerrnl (Pp.hov 0 pps));
+	exit 0
 
     | ("-config" | "--config") :: _ -> Usage.print_config (); exit 0
 
@@ -188,14 +175,15 @@ let parse_args () =
 
 let main () =
   let cfiles, args = parse_args () in
-  if cfiles = [] then begin
-    prerr_endline "coqc: too few arguments" ;
-    usage ()
-  end;
-  let coqtopname = 
-    if !image <> "" then !image else Filename.concat !bindir (!binary ^ Coq_config.exec_extension)
-  in
-(*  List.iter (compile coqtopname args) cfiles*)
-  Unix.handle_unix_error (compile coqtopname args) cfiles
+    if cfiles = [] then begin
+      prerr_endline "coqc: too few arguments" ;
+      usage ()
+    end;
+    let coqtopname = 
+      if !image <> "" then !image 
+      else Filename.concat (Envars.coqbin ()) (!binary ^ Coq_config.exec_extension)
+    in
+      (*  List.iter (compile coqtopname args) cfiles*)
+      Unix.handle_unix_error (compile coqtopname args) cfiles
     
 let _ = Printexc.print main (); exit 0
diff --git a/scripts/coqmktop.ml b/scripts/coqmktop.ml
index 1b9247616..0bd9d0402 100644
--- a/scripts/coqmktop.ml
+++ b/scripts/coqmktop.ml
@@ -17,7 +17,7 @@ open Unix
 (* Objects to link *)
 
 (* 1. Core objects *)
-let ocamlobjs = ["unix.cma";"nums.cma"]
+let ocamlobjs = ["str.cma";"unix.cma";"nums.cma"]
 let dynobjs = ["dynlink.cma"]
 let camlp4objs = ["gramlib.cma"]
 let libobjs = ocamlobjs @ camlp4objs
@@ -44,7 +44,6 @@ let notopobjs = gramobjs
 (* 4. High-level tactics objects *)
 
 (* environment *)
-let src_coqtop = ref Coq_config.coqtop
 let opt        = ref false
 let full       = ref false
 let top        = ref false
@@ -57,11 +56,13 @@ let src_dirs () =
   if !coqide then [[ "ide" ]] else []
 
 let includes () = 
-  List.fold_right
-    (fun d l -> "-I" :: List.fold_left Filename.concat !src_coqtop d :: l)
-    (src_dirs ())
-    (["-I"; "\"" ^ Coq_config.camlp4lib ^ "\""] @ 
-     (if !coqide then ["-thread"; "-I"; "+lablgtk2"] else []))
+  let coqlib = Envars.coqlib () in
+    List.fold_right
+      (fun d l -> "-I" :: List.fold_left Filename.concat coqlib d :: l)
+      (src_dirs ())
+      (["-I"; "\"" ^ Coq_config.camlp4lib ^ "\""] @ 
+	 ["-I"; "\"" ^ coqlib ^ "\""] @
+	 (if !coqide then ["-thread"; "-I"; "+lablgtk2"] else []))
 
 (* Transform bytecode object file names in native object file names *)
 let native_suffix f =
@@ -88,11 +89,11 @@ let files_to_link userfiles =
   let toplevel_objs =
     if !top then topobjs else if !opt then notopobjs else [] in
   let ide_objs = if !coqide then 
-    "str.cma"::"threads.cma"::"lablgtk.cma"::"gtkThread.cmo"::ide 
+    "threads.cma"::"lablgtk.cma"::"gtkThread.cmo"::ide 
   else [] 
   in
   let ide_libs = if !coqide then 
-    ["str.cma" ; "threads.cma" ; "lablgtk.cma" ; "gtkThread.cmo" ;
+    ["threads.cma" ; "lablgtk.cma" ; "gtkThread.cmo" ;
      "ide/ide.cma" ]
   else [] 
   in
@@ -136,22 +137,33 @@ let all_subdirs dir =
 let usage () =
   prerr_endline "Usage: coqmktop <options> <ocaml options> files
 Flags.are:
-  -srcdir dir   Specify where the Coq source files are
-  -o exec-file  Specify the name of the resulting toplevel
-  -opt          Compile in native code
-  -full         Link high level tactics
-  -top          Build Coq on a ocaml toplevel (incompatible with -opt)
-  -searchisos   Build a toplevel for SearchIsos
-  -ide          Build a toplevel for the Coq IDE
-  -R dir        Specify recursively directories for Ocaml\n";
+  -coqlib dir    Specify where the Coq object files are
+  -camlbin dir   Specify where the OCaml binaries are
+  -camlp4bin dir Specify where the CAmp4/5 binaries are
+  -o exec-file   Specify the name of the resulting toplevel
+  -boot          Run in boot mode
+  -opt           Compile in native code
+  -full          Link high level tactics
+  -top           Build Coq on a ocaml toplevel (incompatible with -opt)
+  -searchisos    Build a toplevel for SearchIsos
+  -ide           Build a toplevel for the Coq IDE
+  -R dir         Specify recursively directories for Ocaml\n";
   exit 1
 
 (* parsing of the command line *)
 let parse_args () =
   let rec parse (op,fl) = function
     | [] -> List.rev op, List.rev fl
-    | "-srcdir" :: d :: rem -> src_coqtop := d ; parse (op,fl) rem
-    | "-srcdir" :: _        -> usage ()
+    | "-coqlib" :: d :: rem -> 
+	Flags.coqlib_spec := true; Flags.coqlib := d ; parse (op,fl) rem
+    | "-coqlib" :: _        -> usage ()
+    | "-camlbin" :: d :: rem -> 
+	Flags.camlbin_spec := true; Flags.camlbin := d ; parse (op,fl) rem
+    | "-camlbin" :: _        -> usage ()
+    | "-camlp4bin" :: d :: rem -> 
+	Flags.camlp4bin_spec := true; Flags.camlp4bin := d ; parse (op,fl) rem
+    | "-camlp4bin" :: _        -> usage ()
+    | "-boot" :: rem -> Flags.boot := true; parse (op,fl) rem
     | "-opt" :: rem -> opt := true ; parse (op,fl) rem
     | "-full" :: rem -> full := true ; parse (op,fl) rem
     | "-top" :: rem -> top := true ; parse (op,fl) rem
@@ -254,16 +266,17 @@ let create_tmp_main_file modules =
 let main () =
   let (options, userfiles) = parse_args () in
   (* which ocaml command to invoke *)
+  let camlbin = Envars.camlbin () in
   let prog =
     if !opt then begin
       (* native code *)
       if !top then failwith "no custom toplevel in native code !";
-      let ocamloptexec = Filename.concat Coq_config.camldir "ocamlopt" in
+      let ocamloptexec = Filename.concat camlbin "ocamlopt" in
         ocamloptexec^" -linkall"
     end else
       (* bytecode (we shunt ocamlmktop script which fails on win32) *)
       let ocamlmktoplib = " toplevellib.cma" in
-      let ocamlcexec = Filename.concat Coq_config.camldir "ocamlc" in
+      let ocamlcexec = Filename.concat camlbin "ocamlc" in
       let ocamlccustom = Printf.sprintf "%s %s -linkall "
         ocamlcexec Coq_config.coqrunbyteflags in
       (if !top then ocamlccustom^ocamlmktoplib else ocamlccustom)
@@ -282,22 +295,22 @@ let main () =
   try
     let args =
       options @ (includes ()) @ copts @ tolink @ dynlink @ [ main_file ] in
-    (* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *)
+      (* add topstart.cmo explicitly because we shunted ocamlmktop wrapper *)
     let args = if !top then args @ [ "topstart.cmo" ] else args in
-    (* Now, with the .cma, we MUST use the -linkall option *)
+      (* Now, with the .cma, we MUST use the -linkall option *)
     let command = String.concat " " (prog::"-rectypes"::args) in
-    if !echo then 
-      begin 
-	print_endline command; 
-	print_endline 
-	  ("(command length is " ^ 
-	   (string_of_int (String.length command)) ^ " characters)");
-	flush Pervasives.stdout 
-      end;
-    let retcode = Sys.command command in
-    clean main_file;
-    (* command gives the exit code in HSB, and signal in LSB !!! *)
-    if retcode > 255 then retcode lsr 8 else retcode 
+      if !echo then 
+	begin 
+	  print_endline command; 
+	  print_endline 
+	    ("(command length is " ^ 
+	       (string_of_int (String.length command)) ^ " characters)");
+	  flush Pervasives.stdout 
+	end;
+      let retcode = Sys.command command in
+	clean main_file;
+	(* command gives the exit code in HSB, and signal in LSB !!! *)
+	if retcode > 255 then retcode lsr 8 else retcode 
   with e -> 
     clean main_file; raise e
 
diff --git a/test-suite/check b/test-suite/check
index 68a4b0e38..a73654bcd 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -3,9 +3,9 @@
 # Automatic test of Coq
 
 if [ "$1" = -byte ]; then
-  coqtop="../bin/coqtop.byte -q -batch"
+  coqtop="../bin/coqtop.byte -boot -q -batch"
 else
-  coqtop="../bin/coqtop -q -batch"
+  coqtop="../bin/coqtop -boot -q -batch"
 fi
 
 command="$coqtop -top Top -load-vernac-source"
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 52923ad4e..77fdffb0d 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -89,8 +89,6 @@ let is_genrule r =
       Str.string_match genrule r 0
 
 let standard sds sps =
-  print "Makefile.config:\n";
-  print "\t$(COQBIN)coqtop -config > $@\n\n";
   print "byte:\n";
   print "\t$(MAKE) all \"OPT:=-byte\"\n\n";
   print "opt:\n";
@@ -121,7 +119,7 @@ let standard sds sps =
   print "clean:\n";
   print "\trm -f $(CMOFILES) $(CMIFILES) $(CMXFILES) $(CMXSFILES) $(OFILES) $(VOFILES) $(VIFILES) $(GFILES) $(MLFILES:.ml=.cmo) $(MLFILES:.ml=.cmx) *~\n";
   print "\trm -f all.ps all-gal.ps all.pdf all-gal.pdf all.glob $(VFILES:.v=.glob) $(HTMLFILES) \
-         $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d) Makefile.config\n";
+         $(GHTMLFILES) $(VFILES:.v=.tex) $(VFILES:.v=.g.tex) $(VFILES:.v=.v.d)\n";
   if !some_mlfile then
     print "\trm -f $(CMOFILES) $(MLFILES:.ml=.cmi) $(MLFILES:.ml=.ml.d)\n";
   print "\t- rm -rf html\n";
@@ -139,10 +137,11 @@ let standard sds sps =
   List.iter
     (fun x -> print "\t(cd "; print x; print " ; $(MAKE) archclean)\n")
     sds;
-  print "\n\n"
+  print "\n\n";
+  print "printenv: \n\t@echo CAMLC =\t$(CAMLC)\n\t@echo CAMLOPTC =\t$(CAMLOPTC)\n";
+  print "\t@echo CAMLP4LIB =\t$(CAMLP4LIB)\n\n"
 
-let header_includes () =
-  print "include Makefile.config\n.PHONY: Makefile.config\n"
+let header_includes () = ()
   
 let footer_includes () = 
   if !some_vfile then print "-include $(VFILES:.v=.v.d)\n.SECONDARY: $(VFILES:.v=.v.d)\n\n";
@@ -187,10 +186,12 @@ let variables l =
     if !impredicative_set = true then print "OTHERFLAGS=-impredicative-set\n";
     (* Coq executables and relative variables *)
     print "COQFLAGS:=-q $(OPT) $(COQLIBS) $(OTHERFLAGS) $(COQ_XML)\n";
+    print "ifdef CAMLBIN\n  COQMKTOPFLAGS:=-camlbin $(CAMLBIN) -camlp4bin $(CAMLP4BIN)\nendif\n";
     print "COQC:=$(COQBIN)coqc\n";
     print "COQDEP:=$(COQBIN)coqdep -c\n";
     print "GALLINA:=$(COQBIN)gallina\n";
     print "COQDOC:=$(COQBIN)coqdoc\n";
+    print "COQMKTOP:=$(COQBIN)coqmktop\n";
     (* Caml executables and relative variables *)
     printf "CAMLC:=$(CAMLBIN)%s -rectypes\n" best_ocamlc;
     printf "CAMLOPTC:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt;
@@ -228,11 +229,13 @@ let dir_of_target t =
 
 let parameters () =
   print "# \n";
-  print "# This Makefile looks for coqtop in PATH and in COQBIN to create Makefile.config\n";
-  print "# Once created, Make refers to this file to determine the important paths for Coq\n";
-  print "# and Caml binaries. To change which Coq is used to compile your contribution,\n";
-  print "# delete Makefile.config, and set COQBIN to the desired value.\n";
-  print "# \n\n"
+  print "# This Makefile may take 3 arguments passed as environment variables:\n";
+  print "#   - COQBIN to specify the directory where Coq binaries resides;\n";
+  print "#   - CAMLBIN and CAMLP4BIN to give the path for the OCaml and Camlp4/5 binaries.\n";
+  print "COQLIB:=$(shell $(COQBIN)coqtop -where)\n"; 
+  print "CAMLP4:=$(shell $(COQBIN)coqtop -config | awk -F = '/CAMLP4=/{print $$2}')\n"; 
+  print "ifndef CAMLP4BIN\n  CAMLP4BIN:=$(CAMLBIN)\nendif\n\n";
+  print "CAMLP4LIB:=$(shell $(CAMLP4BIN)$(CAMLP4) -where)\n\n"
 
 let include_dirs l =
   let rec split_includes l = 
@@ -263,22 +266,18 @@ let include_dirs l =
   let str_r = parse_includes inc_r in
     section "Libraries definitions.";
     print "OCAMLLIBS:=-I $(CAMLP4LIB) "; print_list "\\\n  " str_i; print "\n";
-    print "ifneq ($(LOCAL),0) # set COQTOP for compiling from Coq sources\n";
-    print "  COQSRCLIBS:=-I $(COQTOP)/kernel -I $(COQTOP)/lib \\
-  -I $(COQTOP)/library -I $(COQTOP)/parsing \\
-  -I $(COQTOP)/pretyping -I $(COQTOP)/interp \\
-  -I $(COQTOP)/proofs -I $(COQTOP)/tactics \\
-  -I $(COQTOP)/toplevel -I $(COQTOP)/contrib/cc -I $(COQTOP)/contrib/dp \\
-  -I $(COQTOP)/contrib/extraction -I $(COQTOP)/contrib/field \\
-  -I $(COQTOP)/contrib/firstorder -I $(COQTOP)/contrib/fourier \\
-  -I $(COQTOP)/contrib/funind -I $(COQTOP)/contrib/interface \\
-  -I $(COQTOP)/contrib/micromega -I $(COQTOP)/contrib/omega \\
-  -I $(COQTOP)/contrib/ring -I $(COQTOP)/contrib/romega \\
-  -I $(COQTOP)/contrib/rtauto -I $(COQTOP)/contrib/setoid_ring \\
-  -I $(COQTOP)/contrib/subtac -I $(COQTOP)/contrib/xml\n";
-    print "else\n";
-    print "  COQSRCLIBS:=-I $(COQLIB)\n";
-    print "endif\n";
+    print "COQSRCLIBS:=-I $(COQLIB)/kernel -I $(COQLIB)/lib \\
+  -I $(COQLIB)/library -I $(COQLIB)/parsing \\
+  -I $(COQLIB)/pretyping -I $(COQLIB)/interp \\
+  -I $(COQLIB)/proofs -I $(COQLIB)/tactics \\
+  -I $(COQLIB)/toplevel -I $(COQLIB)/contrib/cc -I $(COQLIB)/contrib/dp \\
+  -I $(COQLIB)/contrib/extraction -I $(COQLIB)/contrib/field \\
+  -I $(COQLIB)/contrib/firstorder -I $(COQLIB)/contrib/fourier \\
+  -I $(COQLIB)/contrib/funind -I $(COQLIB)/contrib/interface \\
+  -I $(COQLIB)/contrib/micromega -I $(COQLIB)/contrib/omega \\
+  -I $(COQLIB)/contrib/ring -I $(COQLIB)/contrib/romega \\
+  -I $(COQLIB)/contrib/rtauto -I $(COQLIB)/contrib/setoid_ring \\
+  -I $(COQLIB)/contrib/subtac -I $(COQLIB)/contrib/xml\n";
     print "COQLIBS:="; print_list "\\\n  " str_i'; print " "; print_list "\\\n  " str_r; print "\n";
     print "COQDOCLIBS:=";   print_list "\\\n  " str_r; print "\n\n"
 
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index 3d93c8a90..393554568 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -15,8 +15,6 @@ open Unix
 let stderr = Pervasives.stderr
 let stdout = Pervasives.stdout
 
-let coqlib = ref Coq_config.coqlib
-
 let option_c = ref false
 let option_D = ref false
 let option_w = ref false
@@ -24,7 +22,6 @@ let option_i = ref false
 let option_sort = ref false
 let option_noglob = ref false
 let option_slash = ref false
-let option_boot = ref false
 
 let suffixe = ref ".vo"
 let suffixe_spec = ref ".vi"
@@ -516,14 +513,14 @@ let rec parse = function
   | "-D" :: ll -> option_D := true; parse ll
   | "-w" :: ll -> option_w := true; parse ll
   | "-i" :: ll -> option_i := true; parse ll
-  | "-boot" :: ll -> option_boot := true; parse ll
+  | "-boot" :: ll -> Flags.boot := true; parse ll
   | "-sort" :: ll -> option_sort := true; parse ll
   | "-noglob" :: ll | "-no-glob" :: ll -> option_noglob := true; parse ll
   | "-I" :: r :: ll -> add_dir add_known r []; parse ll
   | "-I" :: [] -> usage ()
   | "-R" :: r :: ln :: ll -> add_rec_dir add_known r [ln]; parse ll
   | "-R" :: ([] | [_]) -> usage ()
-  | "-coqlib" :: (r :: ll) -> coqlib := r; parse ll
+  | "-coqlib" :: (r :: ll) -> Flags.coqlib_spec := true; Flags.coqlib := r; parse ll
   | "-coqlib" :: [] -> usage ()
   | "-suffix" :: (s :: ll) -> suffixe := s ; suffixe_spec := s; parse ll
   | "-suffix" :: [] -> usage ()
@@ -534,13 +531,14 @@ let rec parse = function
 let coqdep () =
   if Array.length Sys.argv < 2 then usage ();
   parse (List.tl (Array.to_list Sys.argv));
-  if !option_boot then begin
+  if !Flags.boot then begin
     add_rec_dir add_known "theories" ["Coq"];
     add_rec_dir add_known "contrib" ["Coq"]
-  end else begin 
-    add_rec_dir add_coqlib_known (!coqlib//"theories") ["Coq"]; 
-    add_rec_dir add_coqlib_known (!coqlib//"contrib") ["Coq"];
-    add_dir add_coqlib_known (!coqlib//"user-contrib") []
+  end else begin
+    let coqlib = Envars.coqlib () in
+      add_rec_dir add_coqlib_known (coqlib//"theories") ["Coq"]; 
+      add_rec_dir add_coqlib_known (coqlib//"contrib") ["Coq"];
+      add_dir add_coqlib_known (coqlib//"user-contrib") []
   end;
   List.iter (fun (f,_,d) -> Hashtbl.add mliKnown f d) !mliAccu;
   List.iter (fun (f,_,d) -> Hashtbl.add mlKnown f d) !mlAccu;
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index e6c3e5c07..864b2718e 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -57,6 +57,7 @@ let usage () =
   prerr_endline "  --no-externals       no links to Coq standard library";
   prerr_endline "  --coqlib <url>       set URL for Coq standard library";
   prerr_endline "                       (default is http://coq.inria.fr/library/)";
+  prerr_endline "  --boot               run in boot mode";
   prerr_endline "  --coqlib_path <dir>  set the path where Coq files are installed";
   prerr_endline "  -R <dir> <coqdir>    map physical dir to Coq dir";
   prerr_endline "  --latin1             set ISO-8859-1 input language";
@@ -318,6 +319,8 @@ let parse () =
 	Cdglobals.coqlib := u; parse_rec rem
     | ("--coqlib" | "-coqlib") :: [] ->
 	usage ()
+    | ("--boot" | "-boot") :: rem ->
+	Cdglobals.coqlib_path := Coq_config.coqsrc; parse_rec rem
     | ("--coqlib_path" | "-coqlib_path") :: d :: rem ->
 	Cdglobals.coqlib_path := d; parse_rec rem
     | ("--coqlib_path" | "-coqlib_path") :: [] ->
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index daae9b94e..a21e33c87 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -93,16 +93,12 @@ let theories_dirs_map = [
     "theories/Init", "Init"
   ]
 
-(* Initializes the LoadPath according to COQLIB and Coq_config *)
+(* Initializes the LoadPath *)
 let init_load_path () =
-  let coqlib =
-    (* variable COQLIB overrides the default library *)
-    getenv_else "COQLIB"
-      (if Coq_config.local || !Flags.boot then Coq_config.coqtop
-	else Coq_config.coqlib) in
+  let coqlib = Envars.coqlib () in
   let user_contrib = coqlib/"user-contrib" in
   let dirs = "states" :: ["contrib"] in
-  let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
+  let camlp4 = Envars.camlp4lib () in
     (* first user-contrib *)
     if Sys.file_exists user_contrib then 
       Mltop.add_rec_path user_contrib Nameops.default_root_prefix;
@@ -129,13 +125,13 @@ let init_library_roots () =
 
 (* Initialises the Ocaml toplevel before launching it, so that it can
    find the "include" file in the *source* directory *)
-(* We only assume that the variable COQTOP is set *)
 let init_ocaml_path () =
-  let coqtop = getenv_else "COQTOP" Coq_config.coqtop in
+  let coqsrc = Coq_config.coqsrc in
   let add_subdir dl = 
-    Mltop.add_ml_dir (List.fold_left (/) coqtop dl) 
+    Mltop.add_ml_dir (List.fold_left (/) coqsrc dl) 
   in
-  List.iter add_subdir
-    [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; 
-      [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ];
-      [ "tactics" ]; [ "toplevel" ]; [ "translate" ]; [ "ide" ] ]
+    Mltop.add_ml_dir (Envars.coqlib ()); 
+    List.iter add_subdir
+      [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; 
+	[ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ];
+	[ "tactics" ]; [ "toplevel" ]; [ "translate" ]; [ "ide" ] ]
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index dd92ccfc2..fec6b0740 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -21,7 +21,7 @@ open Coqinit
 
 let get_version_date () =
   try
-    let ch = open_in (Coq_config.coqlib^"/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)
@@ -274,7 +274,10 @@ let parse_args is_ide =
 	    
     | "-unicode" :: rem -> Flags.unicode_syntax := true; parse rem
 
-    | "-where" :: _ -> print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0
+    | "-coqlib" :: d :: rem -> Flags.coqlib_spec:=true; Flags.coqlib:=d; parse rem
+    | "-coqlib" :: [] -> usage ()
+
+    | "-where" :: _ -> print_endline (Envars.coqlib ()); exit 0
 
     | ("-config"|"--config") :: _ -> Usage.print_config (); exit 0
 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 02fa69142..cdb3b6f02 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -82,7 +82,6 @@ let print_usage_coqc () =
   print_usage "Usage: coqc <options> <Coq options> file...\n
 options are:
   -verbose  compile verbosely
-  -bindir   override the default directory where coqc looks for coqtop
   -image f  specify an alternative executable for Coq
   -t        keep temporary files\n\n"
 
@@ -90,11 +89,12 @@ options are:
 
 let print_config () = 
   if Coq_config.local then Printf.printf "LOCAL=1\n" else Printf.printf "LOCAL=0\n";
-  Printf.printf "COQBIN=%s/\n" Coq_config.bindir;
   Printf.printf "COQLIB=%s/\n" Coq_config.coqlib;
-  Printf.printf "COQTOP=%s/\n" Coq_config.coqtop;
-  Printf.printf "CAMLBIN=%s/\n" Coq_config.camldir;
+  Printf.printf "COQSRC=%s/\n" Coq_config.coqsrc;
+  Printf.printf "CAMLBIN=%s/\n" Coq_config.camlbin;
+  Printf.printf "CAMLLIB=%s/\n" Coq_config.camllib;
   Printf.printf "CAMLP4=%s\n" Coq_config.camlp4;
+  Printf.printf "CAMLP4BIN=%s\n" Coq_config.camlp4bin;
   Printf.printf "CAMLP4LIB=%s\n" Coq_config.camlp4lib