Quelques amendements liées à la compilation des packages.

- typo du configure;
- warnings variables non utilisées dans ide/utils;
- suppression des variables vides COQINSTALLPREFIX et OLDROOT parce
  que l'option -e que l'on aurait pu en principe utiliser pour les
  surcharger ne fonctionne pas lorsqu'il y a plusieurs niveaux
  d'imbrication de makefiles (comme c'est le cas quand on vient
  du makefile servant à faire les packages qui appelle le makefile 
  principal qui appelle les makefile.stage);
- utilisation de ALLVO plutôt qu'un find pour trouver les .v sur
  lesquels appliquer coqdep (permet d'éviter des warning sur les fichiers
  de test, non prévus pour faire partie de la biblio standard);
- utilisation de -custom sur les bytecode qui ne l'étaient pas encore
  (coqchk et coqmktop) pour être indépendant de ocamlrun à
  l'installation.



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

5 files changed, 14 insertions, 16 deletions

diff --git a/Makefile b/Makefile
index 8e992cf4e..d75168272 100644
--- a/Makefile
+++ b/Makefile
@@ -41,8 +41,8 @@ export MLFILES  := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml'  ')' $(FIN
 export MLIFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mli' ')' $(FIND_PRINTF_P)) \
   $(GENMLIFILES)
 export ML4FILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml4' ')' $(FIND_PRINTF_P))
-export VFILES   := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.v'   ')' $(FIND_PRINTF_P)) \
-  $(GENVFILES)
+#export VFILES   := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.v'   ')' $(FIND_PRINTF_P)) \
+#  $(GENVFILES)
 export CFILES   := $(shell find kernel/byterun -name '*.c')
 
 export ML4FILESML:= $(ML4FILES:.ml4=.ml)
diff --git a/Makefile.build b/Makefile.build
index dd2caf8cd..23fdf24cd 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -190,7 +190,7 @@ $(CHICKENOPT): checker/check.cmxa checker/main.ml
 
 $(CHICKENBYTE): checker/check.cma checker/main.ml
 	$(SHOW)'OCAMLC -o $@'
-	$(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -o $@ unix.cma gramlib.cma checker/check.cma checker/main.ml
+	$(HIDE)$(OCAMLC) $(CHKBYTEFLAGS) -custom -o $@ unix.cma gramlib.cma checker/check.cma checker/main.ml
 
 $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN)
 	cd bin && ln -sf coqchk.$(BEST)$(EXE) coqchk$(EXE)
@@ -199,7 +199,7 @@ $(CHICKEN): $(ORDER_ONLY_SEP) $(BESTCHICKEN)
 
 $(COQMKTOPBYTE): $(COQMKTOPCMO)
 	$(SHOW)'OCAMLC -o $@'	
-	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -o $@ str.cma unix.cma \
+	$(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma unix.cma \
           $(COQMKTOPCMO) $(OSDEPLIBS)
 
 $(COQMKTOPOPT): $(COQMKTOPCMX)
@@ -221,7 +221,7 @@ 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) -custom -o $@ unix.cma $(COQCCMO) $(OSDEPLIBS)
 
 $(COQCOPT): $(COQCCMX) $(COQTOPOPT) $(BESTCOQTOP)
 	$(SHOW)'OCAMLOPT -o $@'
@@ -612,8 +612,9 @@ $(MINICOQ): $(MINICOQCMO)
 # Installation
 ###########################################################################
 
-COQINSTALLPREFIX=
-OLDROOT=
+#These variables are intended to be set by the caller to make
+#COQINSTALLPREFIX=
+#OLDROOT=
 
   # Can be changed for a local installation (to make packages).
   # You must NOT put a "/" at the end (Cygnus for win32 does not like "//").
diff --git a/Makefile.common b/Makefile.common
index b76e9aaf6..cba65055a 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -812,6 +812,7 @@ CONTRIBVO:= $(OMEGAVO) $(ROMEGAVO) $(MICROMEGAVO) $(RINGVO) $(FIELDVO) \
 	    $(SUBTACVO) $(RTAUTOVO) $(RECDEFVO) $(NEWRINGVO) $(DPVO)
 
 ALLVO:= $(INITVO) $(THEORIESVO) $(CONTRIBVO)
+VFILES:= $(ALLVO:.vo=.v)
 
 LIBFILES:=$(THEORIESVO) $(CONTRIBVO)
 LIBFILESLIGHT:=$(THEORIESLIGHTVO)
diff --git a/configure b/configure
index c68bc2138..e51cee795 100755
--- a/configure
+++ b/configure
@@ -144,7 +144,7 @@ while : ; do
     -mandir|--mandir) mandir_spec=yes
                       mandir="$2"
 		      shift;;
-    -docdir|--mandir) docdir_spec=yes
+    -docdir|--docdir) docdir_spec=yes
                       docdir="$2"
 		      shift;;
     -emacslib|--emacslib) emacslib_spec=yes
diff --git a/ide/utils/configwin_ihm.ml b/ide/utils/configwin_ihm.ml
index 240fd829d..3ab3823de 100644
--- a/ide/utils/configwin_ihm.ml
+++ b/ide/utils/configwin_ihm.ml
@@ -364,7 +364,7 @@ class string_param_box param (tt:GData.tooltips) =
   let _ = dbg "string_param_box" in
   let hbox = GPack.hbox () in
   let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in
-  let wl = GMisc.label ~text: param.string_label ~packing: wev#add () in
+  let _wl = GMisc.label ~text: param.string_label ~packing: wev#add () in
   let we = GEdit.entry
       ~editable: param.string_editable
       ~packing: (hbox#pack ~expand: param.string_expand ~padding: 2)
@@ -396,7 +396,7 @@ class combo_param_box param (tt:GData.tooltips) =
   let _ = dbg "combo_param_box" in
   let hbox = GPack.hbox () in
   let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in
-  let wl = GMisc.label ~text: param.combo_label ~packing: wev#add () in
+  let _wl = GMisc.label ~text: param.combo_label ~packing: wev#add () in
   let wc = GEdit.combo
       ~popdown_strings: param.combo_choices
       ~value_in_list: (not param.combo_new_allowed)
@@ -754,9 +754,7 @@ class hotkey_param_box param (tt:GData.tooltips) =
   let _ = dbg "hotkey_param_box" in
   let hbox = GPack.hbox () in
   let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in
-  let wl = GMisc.label ~text: param.hk_label
-      ~packing: wev#add ()
-  in
+  let _wl = GMisc.label ~text: param.hk_label ~packing: wev#add () in
   let we = GEdit.entry
       ~editable: false
       ~packing: (hbox#pack ~expand: param.hk_expand ~padding: 2)
@@ -805,9 +803,7 @@ class hotkey_param_box param (tt:GData.tooltips) =
 class modifiers_param_box param =
   let hbox = GPack.hbox () in
   let wev = GBin.event_box ~packing: (hbox#pack ~expand: false ~padding: 2) () in
-  let wl = GMisc.label ~text: param.md_label 
-      ~packing: wev#add () 
-  in
+  let _wl = GMisc.label ~text: param.md_label ~packing: wev#add () in
   let we = GEdit.entry
       ~editable: false
       ~packing: (hbox#pack ~expand: param.md_expand ~padding: 2)