- fixed the Assert_failure error in kernel/modops

- fixed the problem with passing atomic tactics to ltacs
- restructured the distrib Makefile (can build a package from
  the CVS working dir)


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

29 files changed, 648 insertions, 492 deletions

diff --git a/Makefile b/Makefile
index fa86571abc..9963bf7f26 100644
--- a/Makefile
+++ b/Makefile
@@ -620,10 +620,12 @@ install-coqide:: install-ide-$(HASCOQIDE) install-ide-files install-ide-info
 install-ide-no:
 
 install-ide-byte: 
+	$(MKDIR) $(FULLBINDIR)
 	cp $(COQIDEBYTE) $(FULLBINDIR)
 	cd $(FULLBINDIR); ln -sf coqide.byte$(EXE) coqide$(EXE)
 
 install-ide-opt:
+	$(MKDIR) $(FULLBINDIR)
 	cp $(COQIDEBYTE) $(COQIDEOPT) $(FULLBINDIR)
 	cd $(FULLBINDIR); ln -sf coqide.opt$(EXE) coqide$(EXE)
 
@@ -1183,7 +1185,7 @@ install-library7:
 
 install-library-light:
 	$(MKDIR) $(FULLCOQLIB)
-	for f in $(LIBFILESLIGHT) ($NEWLIBFILESLIGHT); do \
+	for f in $(LIBFILESLIGHT) $(NEWLIBFILESLIGHT); do \
 	  $(MKDIR) $(FULLCOQLIB)/`dirname $$f`; \
 	  cp $$f $(FULLCOQLIB)/`dirname $$f`; \
         done
@@ -1574,4 +1576,8 @@ include .depend.coq7
 clean::
 	rm -fr *.v8 states/*.v8 syntax/*.v8 ide/*.v8 \
 	  theories/*/*.v8 theories7/*/*.v8 test-suite/*/*.v8 \
-	  contrib/*/*.v8 contrib7/*/*.v8 \
+	  contrib/*/*.v8 contrib7/*/*.v8
+	find . -name "\.#*" -exec rm -f {} \;
+	find . -name "*~" -exec rm -f {} \;
+
+###########################################################################
diff --git a/contrib/interface/ascent.mli b/contrib/interface/ascent.mli
index ac3f45577e..ae7b71c1c9 100644
--- a/contrib/interface/ascent.mli
+++ b/contrib/interface/ascent.mli
@@ -290,11 +290,11 @@ and ct_FORMULA =
   | CT_elimc of ct_CASE * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA_LIST
   | CT_existvarc
   | CT_fixc of ct_ID * ct_FIX_BINDER_LIST
-  | CT_if of ct_FORMULA * ct_ID_OPT * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA
+  | CT_if of ct_FORMULA * ct_ID_OPT_OPT * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA
   | CT_inductive_let of ct_FORMULA_OPT * ct_ID_OPT_NE_LIST * ct_FORMULA * ct_FORMULA
   | CT_labelled_arg of ct_ID * ct_FORMULA
   | CT_lambdac of ct_BINDER_NE_LIST * ct_FORMULA
-  | CT_let_tuple of ct_ID_OPT_NE_LIST * ct_ID_OPT * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA
+  | CT_let_tuple of ct_ID_OPT_NE_LIST * ct_ID_OPT_OPT * ct_FORMULA_OPT * ct_FORMULA * ct_FORMULA
   | CT_letin of ct_DEF * ct_FORMULA
   | CT_notation of ct_STRING * ct_FORMULA_LIST
   | CT_num_encapsulator of ct_NUM_TYPE * ct_FORMULA
@@ -351,6 +351,10 @@ and ct_ID_OPT_NE_LIST =
 and ct_ID_OPT_OR_ALL =
     CT_coerce_ID_OPT_to_ID_OPT_OR_ALL of ct_ID_OPT
   | CT_all
+and ct_ID_OPT_OPT =
+    CT_coerce_ID_to_ID_OPT_OPT of ct_ID
+  | CT_coerce_ANONYMOUS_to_ID_OPT_OPT of ct_NONE
+  | CT_coerce_NONE_to_ID_OPT_OPT of ct_NONE
 and ct_ID_OR_INT =
     CT_coerce_ID_to_ID_OR_INT of ct_ID
   | CT_coerce_INT_to_ID_OR_INT of ct_INT
diff --git a/contrib/interface/vtp.ml b/contrib/interface/vtp.ml
index 4c3288494e..d758113865 100644
--- a/contrib/interface/vtp.ml
+++ b/contrib/interface/vtp.ml
@@ -802,7 +802,7 @@ and fFORMULA = function
    fNODE "fixc" 2
 | CT_if(x1, x2, x3, x4, x5) ->
    fFORMULA x1;
-   fID_OPT x2;
+   fID_OPT_OPT x2;
    fFORMULA_OPT x3;
    fFORMULA x4;
    fFORMULA x5;
@@ -823,7 +823,7 @@ and fFORMULA = function
    fNODE "lambdac" 2
 | CT_let_tuple(x1, x2, x3, x4, x5) ->
    fID_OPT_NE_LIST x1;
-   fID_OPT x2;
+   fID_OPT_OPT x2;
    fFORMULA_OPT x3;
    fFORMULA x4;
    fFORMULA x5;
@@ -925,6 +925,12 @@ and fID_OPT_NE_LIST = function
    fID_OPT x;
    (List.iter fID_OPT l);
    fNODE "id_opt_ne_list" (1 + (List.length l))
+and fID_OPT_OPT = function
+| CT_coerce_ID_to_ID_OPT_OPT x -> fID x
+| CT_coerce_ANONYMOUS_to_ID_OPT_OPT x ->
+    fNONE x;
+    fNODE "anonymous" 1
+| CT_coerce_NONE_to_ID_OPT_OPT x -> fNONE x
 and fID_OPT_OR_ALL = function
 | CT_coerce_ID_OPT_to_ID_OPT_OR_ALL x -> fID_OPT x
 | CT_all -> fNODE "all" 0
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index cc06b43f3f..4ddcd21503 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -272,11 +272,15 @@ let rec xlate_match_pattern =
 ;;
 
 
+let xlate_id_opt_opt = function
+    Some (Name id) -> CT_coerce_ID_to_ID_OPT_OPT(CT_ident (string_of_id id))
+  | Some Anonymous -> CT_coerce_ANONYMOUS_to_ID_OPT_OPT CT_none
+  | None -> CT_coerce_NONE_to_ID_OPT_OPT CT_none
+
 let xlate_id_opt_aux = function
     Name id -> ctf_ID_OPT_SOME(CT_ident (string_of_id id))
   | Anonymous -> ctv_ID_OPT_NONE;;
 
-
 let xlate_id_opt (_, v) = xlate_id_opt_aux v;;
 
 let xlate_id_opt_ne_list = function
@@ -380,14 +384,14 @@ and (xlate_formula:Topconstr.constr_expr -> Ascent.ct_FORMULA) = function
    | CLetTuple (_,a::l, (na,po), c, b) -> 
       CT_let_tuple(CT_id_opt_ne_list(xlate_id_opt_aux a,
 				     List.map xlate_id_opt_aux l),
-		   xlate_id_opt_aux na,
+		   xlate_id_opt_opt na,
 		   xlate_formula_opt po,
 		   xlate_formula c,
 		   xlate_formula b)
    | CLetTuple (_, [], _, _, _) -> xlate_error "NOT parsed: Let with ()"
    | CIf (_,c, (na, p), b1, b2) -> 
        CT_if
-	 (xlate_formula c, xlate_id_opt_aux na, xlate_formula_opt p,
+	 (xlate_formula c, xlate_id_opt_opt na, xlate_formula_opt p,
 	  xlate_formula b1, xlate_formula b2)
 
    | COrderedCase (_,Term.LetStyle, po, c, [CLambdaN(_,[l,_],b)]) ->
diff --git a/distrib/Makefile b/distrib/Makefile
index 869130f6df..79dcdae715 100644
--- a/distrib/Makefile
+++ b/distrib/Makefile
@@ -1,38 +1,25 @@
 # Building the different files of the coq distribution
 
+# Rk: parameterized targets are not accepted on DEC boxes...
+
+# config.distrib defines: VERSION, PREVIOUSVERSION, DISTRIBDIR,
+# CVSMODULE, CVSTAG, RELEASENUM and ARCH 
 sinclude config.distrib
 LOCALARCH=`uname -m`
 SYSTEM=`uname -s`
 
-ARCHBUILDROOT=$(DISTRIBDIR)/${ARCH}
-RPMTOPDIR=$(DISTRIBDIR)/redhat
-RPMTMPPATHDIR=$(DISTRIBDIR)/redhat/admin
-
-# Parce que le chemin d'installation est cablé en dur dans coqtop, on ne
-# peut pas construire les rpm ailleurs que dans / et donc on doit être root
-#RPMBUILDROOTOPT=
-RPMBUILDROOT=$(DISTRIBDIR)/rpmbuildroot
-RPMBUILDROOTOPT=--buildroot ${RPMBUILDROOT}
-
-# rpm versions 2 and 3: replace rpmbuild by rpm 
-RAWRPM=rpmbuild
-
-RPMVERSION=`${RAWRPM} --version | sed -e "s/RPM version \(.\).*/\1/"`
-RPM=${RAWRPM} ${RPMBUILDROOTOPT} --rcfile rpmrc
+BUILDTARGET=world
+INSTTARGET=install
+MAKECOQ=make
 
+# We assume we are not on pauillac, so we use ssh and scp
+SERVER=pauillac.inria.fr
+CP=scp -p
+SERVEREXEC=ssh $(SERVER) sh -c
 FTPDIR=/net/pauillac/infosystems/ftp/coq/coq
-WWWDIR=/net/pauillac/infosystems/www/coq
-
-COQDEBPACKAGE=coq_${VERSION}-${DEBRELEASENUM}_i386.deb
-
-COQPACKAGE=coq-${VERSION}
-COQRPMPACKAGE=coq-${VERSION}-${RELEASENUM}
-COQDEBPACKAGE=coq_${VERSION}-${RELEASENUM}_i386.deb
-COQDEBCHANGES=coq_${VERSION}-${RELEASENUM}_*.changes
-COQDEBORIG=coq_${VERSION}.orig
+#WWWDIR=/net/pauillac/infosystems/www/coq
 
-COQIDERPMPACKAGE=coqide-${VERSION}-${RELEASENUM}
-COQIDEDEBPACKAGE=coqide_${VERSION}-${RELEASENUM}_i386.deb
+FTPVDIR=$(SERVER):$(FTPDIR)/V$(VERSION)
 
 ######################
 
@@ -40,345 +27,337 @@ noarguments:
 	@echo Please use either
 	@echo "make tag          to tag the current archive with the release number"
 	@echo "make tar-gz       to build a tar.gz of sources"
+	@echo "make arch-tar-gz  to prepare a binary tar.gz for this arch"
 	@echo "make rpm          to prepare a src.rpm and a rpm for the current arch"
 	@echo "make arch-rpm     to prepare a rpm for the current arch from the src.rpm"
-	@echo "make arch-tar-gz  to prepare a binary tar.gz for this arch"
-	@echo "make contrib-tag    to tag the current contrib state with the release number"
-	@echo "make contrib-tar-gz to build a tar.gz of contrib sources"
-	@echo "make ftp-install  to prepare the ftp repository and copy the packages done"
+	@echo "make ide-rpm      to build a src.rpm and a rpm for coqide on this arch"
+	@echo "make ide-arch-rpm to build a rpm for coqide on this arch from the src.rpm"
+	@echo "make deb          to build a debian package"
+	@echo "make win          to build a windows package"
+	@echo "make macosx       to build a MacOS-X package on a disk image"
+	@echo "make contrib-tag     to tag the current contrib state with the release number"
+	@echo "make contrib-tar-gz  to build a tar.gz of contrib sources"
+	@echo "make ftp-install     to prepare the ftp repository and copy the packages done"
 	@echo "make tar-gz-ftp-install         |add the corresponding"
 	@echo "make src-rpm-ftp-install        |packages to the ftp"
 	@echo "make arch-rpm-ftp-install       |repository supposed"
 	@echo "make arch-tar-gz-ftp-install    |to be already"
 	@echo "make contrib-ftp-install	       |prepared"
-	@echo "make deb		 to build a debian package"
-	@echo "make win		 to build a windows package"
-	@echo "make macosx	 to build a MacOS-X package on a disk image"
-	@echo "make ide-rpm      to build a src.rpm and a rpm for coqide on this arch"
-	@echo "make ide-arch-rpm to build a rpm for coqide on this arch from the src.rpm"
+	@echo
+	@echo "make clean        to remove temporary files"
+	@echo "make cleanall     also removes built packages" 
 
 ################## Main targets
 
-distrib: tag export tar-gz
-rpm: src-rpm arch-rpm
-ide-rpm: ide-src-rpm ide-arch-rpm
+COQPACKAGE=coq-$(VERSION)
 
-#################
-tag:
-	echo -n "Tagging the archive with version number $(DASHEDVERSION)...";\
-	cvs rtag -F $(DASHEDVERSION) $(MAJORVERSION)
+distrib: tag tar-gz
+
+###################################################################
+# Tagging the archive
+#
 
-export:
+tag:
+	echo -n "Tagging the archive with version number $(CVSTAG)...";\
+	cvs rtag -F $(CVSTAG) $(CVSMODULE)
+
+
+## Use make LOCAL=1 to build packages from working directory...
+ifeq ($(LOCAL),1)
+# export sources of the current work directory
+WORKDIR=..
+$(COQPACKAGE):
+	@echo "Copying sources from work directory"
+	@- rm -rf $(COQPACKAGE)
+	mkdir $(COQPACKAGE)
+	cd $(WORKDIR) ; cp -rf `ls -a | egrep -v 'distrib|^\.$$|^\.\.$$'` $(DISTRIBDIR)/$(COQPACKAGE)/
+	cd $(COQPACKAGE)/ ; $(MAKECOQ) clean; \
+	  rm -fr CVS */CVS */*/CVS */*/*/CVS */*/*/*/CVS
+	find $(COQPACKAGE) -name CVS -type d -exec rm -fr {} \;
+else
+# export a fresh copy of the tagged CVS version
+$(COQPACKAGE):
 	@echo -n Exporting a fresh copy of the archive...
-	@- rm -rf ${COQPACKAGE}
-	@cvs export -d $(COQPACKAGE) -r $(DASHEDVERSION) $(MAJORVERSION)
+	@- rm -rf $(COQPACKAGE)
+	@cvs export -d $(COQPACKAGE) -r $(CVSTAG) $(CVSMODULE)
 	@echo done
-
-export-from-local:
-	@- rm -rf ${COQPACKAGE}
-	mkdir ${COQPACKAGE}
-	cd .. ; cp -rf `ls -a | egrep -v 'distrib|^\.$$|^\.\.$$'` distrib/${COQPACKAGE}/
-	cd ${COQPACKAGE}/ ; $(MAKE) clean
-
-tar-gz: 
-	@echo -n Removing the maintenance files and doc...
-#	@rm -rf ${COQPACKAGE}/doc     # doc is implementation doc
-	@rm -rf ${COQPACKAGE}/distrib
-	@rm -rf ${COQPACKAGE}/KNOWN-BUGS
-	@rm -rf ${COQPACKAGE}/{TODO,ANNONCE,PROBLEMES}
-	@rm -rf ${COQPACKAGE}/theories/Num
-	@rm -rf ${COQPACKAGE}/contrib/graphs
-	@rm -rf ${COQPACKAGE}/doc/newsyntax.tex 
-	@rm -f ${COQPACKAGE}/make.result
-	@rm -rf ${COQPACKAGE}/test-suite/parser   # tests pcoq
-	@find ${COQPACKAGE} -name ".cvsignore" -exec rm {} \;
+endif
+
+###################################################################
+# .tar.gz packages (sources, binaries)
+#
+
+TARGZ=$(COQPACKAGE).tar.gz
+ARCHTAR=$(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar
+ARCHTARGZ=$(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar.gz
+
+tar-gz:
+	rm -f $(TARGZ)
+	$(MAKE) $(TARGZ)
+
+$(TARGZ): $(COQPACKAGE)
+	@rm -rf $(COQPACKAGE)/doc     # doc is implementation doc
+	@rm -rf $(COQPACKAGE)/distrib
+	@rm -rf $(COQPACKAGE)/KNOWN-BUGS
+	@rm -rf $(COQPACKAGE)/{TODO,ANNONCE,PROBLEMES}
+	@rm -rf $(COQPACKAGE)/theories/Num
+	@rm -rf $(COQPACKAGE)/contrib/graphs
+	@rm -rf $(COQPACKAGE)/doc/newsyntax.tex 
+	@rm -f $(COQPACKAGE)/make.result
+	@rm -rf $(COQPACKAGE)/test-suite/parser   # tests pcoq
+	@find $(COQPACKAGE) -name ".cvsignore" -exec rm {} \;
 	@echo done
 	@echo -n Building the tar.gz source package
-	@tar cvf ${COQPACKAGE}.tar ${COQPACKAGE}
-	@gzip --best --force ${COQPACKAGE}.tar
+	@tar cvf $(COQPACKAGE).tar $(COQPACKAGE)
+	@gzip --best --force $(COQPACKAGE).tar
+	@chmod g+w $(TARGZ)
 	@echo done
 	@echo Checking release parameters
 	./check-list
 	@echo done
 
-src-rpm: ${COQRPMPACKAGE}.src.rpm
-arch-rpm: ${COQRPMPACKAGE}.${ARCH}.rpm
-
-ide-src-rpm: ${COQIDERPMPACKAGE}.src.rpm
-ide-arch-rpm: ${COQIDERPMPACKAGE}.${ARCH}.rpm
-
 test:
-	cp ${COQPACKAGE}.tar.gz tmp.tar.gz
-	gunzip tmp.tar.gz
-	@echo Trying "make world check"
-	- rm -rf ${COQPACKAGE}
+	- rm -rf $(COQPACKAGE)
+	gunzip -c $(TARGZ) > tmp.tar
 	tar xf tmp.tar
-	(cd ${COQPACKAGE};\
-	./configure -local -opt -emacs emacs;\
-	make world check >& log.world;\
-	if [ $$? = 0 ];\
-	then echo '"make world check" succeeded';\
-	else echo '"make world check" failed'; exit 1;\
-	fi)
-	rm tmp.tar
+	rm -f tmp.tar
+	@echo Trying "$(MAKECOQ) $(BUILDTARGET) check"
+	(cd $(COQPACKAGE);\
+	 ./configure -local -opt -emacs emacs;\
+	 $(MAKECOQ) world check >& test.log;\
+	 if [ $$? = 0 ];\
+	 then echo '"$(MAKECOQ) $(BUILDTARGET) check" succeeded';\
+	 else echo '"$(MAKECOQ) $(BUILDTARGET) check" failed'; exit 1;\
+	 fi)
 	@echo "Compilation succeeded"
 
-release-bin:
-	@echo
-	@echo "***************"
-	@echo "   attention   "
-	@echo "***************"
-	@echo
-	@echo "   \"make release-bin\" suppose que vous venez de compiler"
-	@echo "   ET D'INSTALLER Coq. Tapez <Ctrl-C> pour abandonner"
-	@echo "   et <Return> pour continuer."
-	@echo
-	@read
-	tar -cvf $(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar --files-from $(COQLIB)/COQFILES
-	gzip --best $(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar
-
-arch-tar-gz-final:
-	(cd ${ARCHBUILDROOT}/buildroot;\
-	tar -cvf ${DISTRIBDIR}/$(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar *)
-	gzip --best $(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar
+# where binaries are compiled
+ARCHBUILDROOT=$(DISTRIBDIR)/tar-$(ARCH)
+ARCHINSTALL=$(ARCHBUILDROOT)/buildroot
 
 arch-tar-gz:
 	$(MAKE) arch-image
 	$(MAKE) arch-tar-gz-final
 
-arch-image: ${COQPACKAGE}.tar.gz
-	@echo "Building $(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar.gz to be installed in /usr/local/"
-	@echo "Warning: leading / is removed"
-	- mkdir -p ${ARCHBUILDROOT}
-	(cd ${ARCHBUILDROOT};\
-	rm -rf ${COQPACKAGE} || true;\
-	gunzip -c $(DISTRIBDIR)/${COQPACKAGE}.tar.gz | tar xf -;\
-	cd ${COQPACKAGE};\
-	./configure -bindir /usr/local/bin -libdir /usr/local/lib/coq -mandir /usr/local/man -emacs emacs -emacslib /usr/local/lib/emacs/site-lisp -opt -reals all -coqide no;\
-	make world check;\
-	rm -rf ${ARCHBUILDROOT}/buildroot/* || true;\
-	make -e COQINSTALLPREFIX=${ARCHBUILDROOT}/buildroot/ install)
-
-win: ${COQPACKAGE}.tar.gz
-	@echo "Building $(COQPACKAGE)-Win.zip to be installed in \coq\bin"
+arch-image: $(TARGZ)
+	@echo "Building $(ARCHTARGZ) to be installed in /usr/local/"
 	@echo "Warning: leading / is removed"
-	- mkdir -p ${ARCHBUILDROOT}
-	(cd ${ARCHBUILDROOT};\
-	rm -rf ${COQPACKAGE} || true;\
-	gunzip -c $(DISTRIBDIR)/${COQPACKAGE}.tar.gz | tar xf -;\
-	cd ${COQPACKAGE};\
-	./configure -bindir /coq/bin -libdir /coq/lib -mandir /coq/man -emacslib /coq/emacs -reals all -coqide no;\
-	make world;\
-	rm -rf ${ARCHBUILDROOT}/buildroot/* || true;\
-	make -e COQINSTALLPREFIX=${ARCHBUILDROOT}/buildroot/ install;\
-	cd ${ARCHBUILDROOT}/buildroot;\
-	mv ../$(COQPACKAGE)/INSTALL.win .;\
-	zip -A -r $(COQPACKAGE)-win.zip *;\
-	mv $(COQPACKAGE)-Win.zip ../..)
-
-rpm-dirs:
-	- mkdir ${RPMTOPDIR}
-	- mkdir ${RPMTOPDIR}/BUILD
-	- mkdir ${RPMTOPDIR}/RPMS
-	- mkdir ${RPMTOPDIR}/SOURCES
-	- mkdir ${RPMTOPDIR}/SPECS
-	- mkdir ${RPMTOPDIR}/SRPMS
-	- mkdir ${RPMTMPPATHDIR}
-	- mkdir ${RPMBUILDROOT}
-
-rpm-config: rpm-dirs
-	- rm rpmrc rpmmacros
-	(if [ "${RPMVERSION}" != "2" ];\
-	then\
-	echo %_topdir ${RPMTOPDIR} > rpmmacros;\
-	echo %_tmppath ${RPMTMPPATHDIR} >> rpmmacros;\
-	echo %_arch ${ARCH} >> rpmmacros;\
-	echo macrofiles:/usr/lib/rpm/macros:rpmmacros > rpmrc;\
-	else\
-	echo topdir: ${RPMTOPDIR} > rpmrc;\
-	echo tmppath: ${RPMTMPPATHDIR} >> rpmrc;\
-	fi)
+	@-rm -fr $(ARCHINSTALL) $(ARCHBUILDROOT)
+	@mkdir -p $(ARCHBUILDROOT) $(ARCHINSTALL)
+	@echo Building binaries... (see arch-image.log)
+	(cd $(ARCHBUILDROOT);\
+	 gunzip -c $(DISTRIBDIR)/$(TARGZ) | tar xf -;\
+	 cd $(COQPACKAGE);\
+	 ./configure -bindir /usr/local/bin -libdir /usr/local/lib/coq -mandir /usr/local/man -emacs emacs -emacslib /usr/local/lib/emacs/site-lisp -opt -reals all -coqide no;\
+	 $(MAKECOQ) coq check;\
+	 $(MAKECOQ) -e COQINSTALLPREFIX=$(ARCHINSTALL) install-coq) > arch-image.log 2>&1
+	@echo " .... done"
 
-# Les cibles suivantes ne sont pas acceptées sur DEC (car paramétrées)
-
-${COQPACKAGE}.tar.gz:
-	${MAKE} export tar-gz
-
-# rpm 3.0 met dans LOCALARCH mais rpm 2.5 dans ARCH...
-${COQRPMPACKAGE}.src.rpm: ${COQPACKAGE}.tar.gz RH/coq.spec
-	${MAKE} rpm-config
-	cp -f petit-coq.gif ${RPMTOPDIR}/SOURCES
-	cp -f ${COQPACKAGE}.tar.gz ${RPMTOPDIR}/SOURCES
-	- mkdir ${RPMTOPDIR}/RPMS/${ARCH}
-	- rm ${RPMTOPDIR}/RPMS/${LOCALARCH}
-	- ln -s ${RPMTOPDIR}/RPMS/${ARCH} ${RPMTOPDIR}/RPMS/${LOCALARCH}
-	- rm -fr $(RPMBUILDROOT)
-	${RPM} -ba RH/coq.spec
-	mv ${RPMTOPDIR}/SRPMS/${COQRPMPACKAGE}.src.rpm .
-	(if [ -f ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${LOCALARCH}.rpm ];\
-	then mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${LOCALARCH}.rpm ${COQRPMPACKAGE}.${ARCH}.rpm;\
-	else mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${ARCH}.rpm .;\
-	fi)
+arch-tar-gz-final:
+	(cd $(ARCHBUILDROOT)/buildroot;\
+	 tar -cvf $(DISTRIBDIR)/$(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar *)
+	gzip --best $(COQPACKAGE)-$(SYSTEM)-$(ARCH).tar
+	chmod g+w $(ARCHTARGZ)
 
-${COQIDERPMPACKAGE}.src.rpm: ${COQPACKAGE}.tar.gz RH/coqide.spec
-	${MAKE} rpm-config
-	cp -f petit-coq.gif ${RPMTOPDIR}/SOURCES
-	cp -f ${COQPACKAGE}.tar.gz ${RPMTOPDIR}/SOURCES
-	- mkdir ${RPMTOPDIR}/RPMS/${ARCH}
-	- rm ${RPMTOPDIR}/RPMS/${LOCALARCH}
-	- ln -s ${RPMTOPDIR}/RPMS/${ARCH} ${RPMTOPDIR}/RPMS/${LOCALARCH}
-	- rm -fr $(RPMBUILDROOT)
-	${RPM} -ba RH/coqide.spec
-	mv ${RPMTOPDIR}/SRPMS/${COQIDERPMPACKAGE}.src.rpm .
-	(if [ -f ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${LOCALARCH}.rpm ];\
-	then mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${LOCALARCH}.rpm ${COQIDERPMPACKAGE}.${ARCH}.rpm;\
-	else mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${ARCH}.rpm .;\
-	fi)
+clean::
+	rm -fr $(ARCHINSTALL) $(ARCHBUILDROOT)
 
-# Sera déjà fait si le src.rpm vient d'être fait
-${COQRPMPACKAGE}.${ARCH}.rpm: rpm-config ${COQRPMPACKAGE}.src.rpm
-	- mkdir ${RPMTOPDIR}/RPMS/${ARCH}
-	- rm ${RPMTOPDIR}/RPMS/${LOCALARCH}
-	- ln -s ${RPMTOPDIR}/RPMS/${ARCH} ${RPMTOPDIR}/RPMS/${LOCALARCH}
-	#- rm -fr $(RPMBUILDROOT)
-	${RPM} --rebuild ${COQRPMPACKAGE}.src.rpm
-	(if [ -f ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${LOCALARCH}.rpm ];\
-	then mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${LOCALARCH}.rpm ${COQRPMPACKAGE}.${ARCH}.rpm;\
-	else mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQRPMPACKAGE}.${ARCH}.rpm .;\
-	fi)
+cleanall::
+	rm -f $(COQPACKAGE) $(TARGZ) $(ARCHTARGZ) arch-image.log test.log
+
+###################################################################
+# RPM (Coq and CoqIde are separated)
+#
+
+rpm: src-rpm arch-rpm
+ide-rpm: ide-src-rpm ide-arch-rpm
+
+RPMTOPDIR=$(DISTRIBDIR)/RH/src
+RPMTMPPATHDIR=$(RPMTOPDIR)/admin
+RPMBUILDROOT=$(RPMTOPDIR)/install
 
-${COQIDERPMPACKAGE}.${ARCH}.rpm: rpm-config ${COQIDERPMPACKAGE}.src.rpm
-	- mkdir ${RPMTOPDIR}/RPMS/${ARCH}
-	- rm ${RPMTOPDIR}/RPMS/${LOCALARCH}
-	- ln -s ${RPMTOPDIR}/RPMS/${ARCH} ${RPMTOPDIR}/RPMS/${LOCALARCH}
-	#- rm -fr $(RPMBUILDROOT)
-	${RPM} --rebuild ${COQIDERPMPACKAGE}.src.rpm
-	(if [ -f ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${LOCALARCH}.rpm ];\
-	then mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${LOCALARCH}.rpm ${COQIDERPMPACKAGE}.${ARCH}.rpm;\
-	else mv ${RPMTOPDIR}/RPMS/${ARCH}/${COQIDERPMPACKAGE}.${ARCH}.rpm .;\
+# rpm versions 2 and 3: replace rpmbuild by rpm 
+RAWRPM=rpmbuild
+RPMVERSION=`$(RAWRPM) --version | sed -e "s/RPM version \(.\).*/\1/"`
+
+# option --target avoids problem with i386/i686
+RPM=$(RAWRPM) --buildroot $(RPMBUILDROOT) --target $(ARCH) --rcfile RH/rpmrc
+
+# rpm files
+COQRPMPACKAGE=coq-$(VERSION)-$(RELEASENUM)
+COQIDERPMPACKAGE=coqide-$(VERSION)-$(RELEASENUM)
+COQSRCRPM=$(COQRPMPACKAGE).src.rpm
+COQRPM=$(COQRPMPACKAGE).$(ARCH).rpm
+COQIDESRCRPM=$(COQIDERPMPACKAGE).src.rpm
+COQIDERPM=$(COQIDERPMPACKAGE).$(ARCH).rpm
+
+RPMLOG=$(DISTRIBDIR)/RH/rpm.log
+RPMFILESLOG=$(DISTRIBDIR)/RH/coqfiles.log
+
+src-rpm: $(COQSRCRPM)
+arch-rpm: $(COQRPM)
+
+ide-src-rpm: $(COQIDESRCRPM)
+ide-arch-rpm: $(COQIDERPM)
+
+$(RPMTOPDIR):
+	@mkdir -p $(RPMTOPDIR)/BUILD
+	@mkdir -p $(RPMTOPDIR)/RPMS
+	@mkdir -p $(RPMTOPDIR)/SOURCES
+	@mkdir -p $(RPMTOPDIR)/SPECS
+	@mkdir -p $(RPMTOPDIR)/SRPMS
+	@mkdir -p $(RPMTMPPATHDIR)
+	@mkdir -p $(RPMTOPDIR)/RPMS/$(ARCH)
+
+RH/rpmrc: config.distrib
+	(if [ "$(RPMVERSION)" != "2" ];\
+	then\
+	echo %_topdir $(RPMTOPDIR) > RH/rpmmacros;\
+	echo %_tmppath $(RPMTMPPATHDIR) >> RH/rpmmacros;\
+	echo %_arch $(ARCH) >> RH/rpmmacros;\
+	echo macrofiles:/usr/lib/rpm/macros:RH/rpmmacros > RH/rpmrc;\
+	else\
+	echo topdir: $(RPMTOPDIR) > RH/rpmrc;\
+	echo tmppath: $(RPMTMPPATHDIR) >> RH/rpmrc;\
 	fi)
 
-RH/coq.list: ${COQPACKAGE}.tar.gz Makefile config.distrib
-	rm -rf RH/${COQPACKAGE} RH/build
-	cd RH ; tar xzf ../${COQPACKAGE}.tar.gz
-	cd RH/${COQPACKAGE} ; sh ../do_build
-	cd RH/${COQPACKAGE} ; make COQINSTALLPREFIX=${DISTRIBDIR}/RH/build install-coq
+$(COQSRCRPM): $(RPMTOPDIR) RH/coq.spec RH/coq.list $(TARGZ) RH/rpmrc
+	cp -f petit-coq.gif $(RPMTOPDIR)/SOURCES
+	cp -f $(TARGZ) $(RPMTOPDIR)/SOURCES
+	cp -f RH/coq.list $(RPMTOPDIR)
+	$(RPM) -bs RH/coq.spec
+	mv $(RPMTOPDIR)/SRPMS/$(COQSRCRPM) .
+	chmod g+w $(COQSRCRPM)
+	rm -fr $(RPMTOPDIR)/SOURCES/* $(RPMTOPDIR)/coq.list
+
+$(COQRPM): $(COQSRCRPM)
+	@-rm -fr $(RPMBUILDROOT)
+	@mkdir -p $(RPMBUILDROOT)
+	@echo "Building the $(ARCH) rpms... (see RH/rpm.log)"
+	cp -f RH/coq.list $(RPMTOPDIR)
+	$(RPM) --rebuild $(COQSRCRPM)
+	mv $(RPMTOPDIR)/RPMS/$(ARCH)/$(COQRPM) .
+	chmod g+w $(COQRPM)
+	rm -f $(RPMTOPDIR)/coq.list
+
+$(COQIDESRCRPM): $(RPMTOPDIR) RH/coqide.spec $(TARGZ) RH/rpmrc
+	cp -f petit-coq.gif $(RPMTOPDIR)/SOURCES
+	cp -f $(TARGZ) $(RPMTOPDIR)/SOURCES
+	$(RPM) -bs RH/coqide.spec
+	mv $(RPMTOPDIR)/SRPMS/$(COQIDESRCRPM) .
+	chmod g+w $(COQIDESRCRPM)
+	rm -fr $(RPMTOPDIR)/SOURCES/*
+
+$(COQIDERPM): $(COQIDESRCRPM)
+	@-rm -fr $(RPMBUILDROOT)
+	@mkdir -p $(RPMBUILDROOT)
+	@echo "Building the $(ARCH) rpms... (see RH/rpm.log)"
+	$(RPM) --rebuild $(COQIDESRCRPM)
+	mv $(RPMTOPDIR)/RPMS/$(ARCH)/$(COQIDERPM) .
+	chmod g+w $(COQIDERPM)
+
+RH/coq.list: $(TARGZ) config.distrib
+	rm -rf RH/$(COQPACKAGE) RH/build
+	cd RH ; tar xzf ../$(TARGZ)
+	@echo "Building coq files list... (see RH/coqfiles.log)"
+	cd RH/$(COQPACKAGE) ; sh ../do_build > $(RPMFILESLOG)
+	cd RH/$(COQPACKAGE) ; $(MAKECOQ) COQINSTALLPREFIX=$(DISTRIBDIR)/RH/build install-coq >> $(RPMFILESLOG)
+	@echo " ... done"
 	echo "# This file has been generated" > RH/coq.list
 	echo "# Do not edit" >>RH/coq.list
 	cd RH/build ; find . '!' -type d | sed -e 's|^\./|/|g' >> ../coq.list
+	rm -rf RH/$(COQPACKAGE) RH/build
 
-RH/coq.spec: RH/coq.list RH/coq.spec.tpl
-	echo "# This file has been generated from RH/coq.spec.tpl" > RH/coq.spec
-	echo "# Do not edit" >> RH/coq.spec
-	cd RH ; m4 -P coq.spec.tpl >> coq.spec
+clean::
+	rm -fr $(RPMTOPDIR) RH/coq.list RH/$(COQPACKAGE) RH/build RH/rpmmacros RH/rpmrc
 
-##########
-contrib-tag:
-	echo -n "Tagging the contrib with version number $(DASHEDVERSION)...";\
-	cvs rtag -F $(DASHEDVERSION) contrib
-	@echo done
+cleanall::
+	rm -f $(COQSRCRPM) $(COQRPM) $(COQIDESRCRPM) $(COQIDERPM) $(RPMLOG) $(RPMFILESLOG)
 
-contrib-tar-gz:
-	- rm -rf contrib-${VERSION}
-	@echo -n Exporting a fresh copy of the contribs...
-	cvs export -d contrib-${VERSION} -r $(DASHEDVERSION) contrib
-	@echo -n Removing the maintenance files ...
-	@rm -rf contrib-${VERSION}/*/*/bench.log
-	@rm -rf contrib-${VERSION}/Lyon/PROGRAMS
-	@find contrib-${VERSION} -name ".cvsignore" -exec rm {} \;
-	@echo done
-	- rm contrib-${VERSION}.tar.gz
-	@echo -n Building the tar.gz contrib package
-	@tar cvf contrib-${VERSION}.tar contrib-${VERSION}
-	@gzip --best contrib-${VERSION}.tar
-	@echo done
+###################################################################
+# Zip for Windows (package does not contain coqide)
+#
 
-##########
-patch:
-	@echo ******** ATTENTION, plante sur pc-linux, essayez pauillac ******
-	cp $(FTPDIR)/V$(PREVIOUSVERSION)/coq-$(PREVIOUSVERSION).tar.gz .
-	rm -rf coq-$(PREVIOUSVERSION)
-	gunzip -c coq-$(PREVIOUSVERSION).tar.gz | tar x
-	rm -rf ${COQPACKAGE}
-	gunzip -c ${COQPACKAGE}.tar.gz | tar x
-	diff -rc coq-$(PREVIOUSVERSION) ${COQPACKAGE} > patch-${VERSION}-$(PREVIOUSVERSION)
-	gzip --best patch-${VERSION}-$(PREVIOUSVERSION)
+COQWINZIP=$(COQPACKAGE)-Win.zip
+WINBUILDROOT=$(DISTRIBDIR)/winbuildroot
+WININSTALL=$(DISTRIBDIR)/wininstallroot
 
-##########
-clean:
-	- rm -rf ${COQPACKAGE} ${RPMTOPDIR} ${ARCHBUILDROOT} ${RPMBUILDROOT} RH/build RH/${COQPACKAGE}
 
-cleanall:
-	- rm -rf ${COQPACKAGE}* ${RPMTOPDIR} ${ARCHBUILDROOT} ${RPMBUILDROOT} 
+win: $(COQWINZIP)
 
-########## Installation in the ftp repository
+$(COQWINZIP): $(TARGZ)
+	@echo "Building $(COQWINZIP) to be installed in \coq\bin"
+	@echo "Warning: leading / is removed"
+	@-rm -fr $(WINBUILDROOT) $(WININSTALL)
+	@-mkdir -p $(WINBUILDROOT) $(WININSTALL)
+	@echo "Compiling and installing coq... (see win.log)"
+	(cd $(WINBUILDROOT);\
+	 gunzip -c $(DISTRIBDIR)/$(TARGZ) | tar xf -;\
+	 cd $(COQPACKAGE);\
+	 ./configure -bindir /coq/bin -libdir /coq/lib -mandir /coq/man -emacslib /coq/emacs -reals all -coqide no;\
+	 $(MAKECOQ) coq;\
+	 $(MAKECOQ) -e COQINSTALLPREFIX=$(WININSTALL) install-coq) > win.log
+	mv $(WINBUILDROOT)/$(COQPACKAGE)/INSTALL.win $(WININSTALL)
+	cd $(WININSTALL); zip -A -r $(DISTRIBDIR)/$(COQWINZIP) *
+
+clean::
+	rm -fr $(WINBUILDROOT) $(WININSTALL)
+
+cleanall::
+	rm -f $(COQWINZIP) win.log
+
+###################################################################
+# Debian
+#
+
+COQDEBPACKAGE=coq_$(VERSION)-$(RELEASENUM)_i386.deb
+COQDEBCHANGES=coq_$(VERSION)-$(RELEASENUM)_*.changes
+COQDEBORIG=coq_$(VERSION).orig
+COQDEBTARGZ=$(COQDEBORIG).tar.gz
+COQIDEDEBPACKAGE=coqide_$(VERSION)-$(RELEASENUM)_i386.deb
+
+DEBIANBUILD=$(DISTRIBDIR)/deb/build
+DEBIANLOG=$(DISTRIBDIR)/deb/deb.log
+LINTIANLOG=$(DISTRIBDIR)/deb/lintian.log
 
-ftp-install: prep-ftp-install
-	cp ${COQPACKAGE}/CHANGES ${FTPDIR}/V${VERSION}/
-	cp ${COQPACKAGE}/README ${FTPDIR}/V${VERSION}/
-	cp ${COQPACKAGE}/README.win ${FTPDIR}/V${VERSION}/
-	cp ${COQPACKAGE}/README.macosx ${FTPDIR}/V${VERSION}/
-	cp ${COQPACKAGE}.tar.gz ${FTPDIR}/V${VERSION}/
-	chmod g+w ${FTPDIR}/V${VERSION}/${COQPACKAGE}.tar.gz
-	cp ${COQPACKAGE}-*.tar.gz ${FTPDIR}/V${VERSION}/
-	chmod g+w ${FTPDIR}/V${VERSION}/${COQPACKAGE}-*.tar.gz
-	cp ${COQRPMPACKAGE}.*.rpm ${FTPDIR}/V${VERSION}/
-	chmod g+w ${FTPDIR}/V${VERSION}/${COQRPMPACKAGE}.*.rpm
-
-# prep-ftp-install: $(FTPDIR)/V${VERSION}
-prep-ftp-install: 
-	- mkdir $(FTPDIR)/V${VERSION}
-	- chmod g+w ${FTPDIR}/V${VERSION}
+deb: prep-deb
+	cd $(DEBIANBUILD)/$(COQPACKAGE) ;\
+	 dpkg-buildpackage -rfakeroot -uc -us 2>&1 | tee $(DEBIANLOG)
+	(lintian $(DEBIANBUILD)/$(COQDEBCHANGES) | tee $(LINTIANLOG)) || true
+
+$(COQDEBTARGZ): $(TARGZ)
+	tar xzf $(TARGZ)
+	mv $(COQPACKAGE) $(COQDEBORIG)
+	tar czf $(COQDEBTARGZ) $(COQDEBORIG)	
+	rm -rf $(COQDEBORIG)
+
+prep-deb: $(COQDEBTARGZ) $(TARGZ)
+	@rm -rf $(DEBIANBUILD)
+	@mkdir -p $(DEBIANBUILD)
+	cp $(COQDEBTARGZ) $(DEBIANBUILD)
+	cd $(DEBIANBUILD) ; tar xzf $(DISTRIBDIR)/$(TARGZ)
+	cp -a debian $(DEBIANBUILD)/$(COQPACKAGE)
+	rm -rf $(DEBIANBUILD)/$(COQPACKAGE)/debian/CVS
+	date > prep-deb
 
-final-ftp-install:
-	(cd $(FTPDIR); rm -f current;ln -sf V${VERSION} current)
+deb-sign: prep-deb
+	cd $(DEBIANBUILD)/$(COQPACKAGE) ;\
+	 dpkg-buildpackage -rfakeroot 2>&1 | tee $(DEBIANLOG)
+	(lintian $(DEBIANBUILD)/$(COQDEBCHANGES) | tee $(LINTIANLOG)) || true
 
-tar-gz-ftp-install: prep-ftp-install
-	cp ${COQPACKAGE}.tar.gz ${FTPDIR}/V${VERSION}/
-	chmod g+w ${FTPDIR}/V${VERSION}/${COQPACKAGE}.tar.gz
 
-src-rpm-ftp-install: prep-ftp-install
-	cp ${COQRPMPACKAGE}.src.rpm ${FTPDIR}/V${VERSION}/
-	chmod g+w ${FTPDIR}/V${VERSION}/${COQRPMPACKAGE}.src.rpm
+clean::
+	rm -fr $(DEBIANBUILD)
 
-arch-rpm-ftp-install: prep-ftp-install
-	cp ${COQRPMPACKAGE}.${ARCH}.rpm ${FTPDIR}/V${VERSION}/
-	chmod g+w ${FTPDIR}/V${VERSION}/${COQRPMPACKAGE}.${ARCH}.rpm
+cleanall::
+	rm -f $(DEBIANLOG) $(LINTIANLOG)
 
-arch-tar-gz-ftp-install: prep-ftp-install
-	cp ${COQPACKAGE}-$(SYSTEM)-$(ARCH).tar.gz ${FTPDIR}/V${VERSION}/
-	chmod g+w ${FTPDIR}/V${VERSION}/${COQPACKAGE}-$(SYSTEM)-$(ARCH).tar.gz
+###################################################################
+# Mac OS X
+#
 
-contrib-ftp-install: prep-ftp-install
-	cp contrib-${VERSION}.tar.gz ${FTPDIR}/V${VERSION}/
-	chmod g+w ${FTPDIR}/V${VERSION}/contrib-${VERSION}.tar.gz
-
-patch-ftp-install: prep-ftp-install
-	cp patch-${VERSION}-$(PREVIOUSVERSION).gz ${FTPDIR}/V${VERSION}/
-	chmod g+w ${FTPDIR}/V${VERSION}/patch-${VERSION}-$(PREVIOUSVERSION).gz
-
-${COQDEBORIG}.tar.gz: ${COQPACKAGE}.tar.gz
-	tar xzf ${COQPACKAGE}.tar.gz
-	mv ${COQPACKAGE} ${COQDEBORIG}
-	tar czf ${COQDEBORIG}.tar.gz ${COQDEBORIG}	
-	rm -rf ${COQDEBORIG}
-
-prep-deb: ${COQDEBORIG}.tar.gz ${COQPACKAGE}.tar.gz
-	rm -rf deb_build
-	mkdir -p deb_build
-	cd deb_build ; cp ../${COQDEBORIG}.tar.gz .
-	cd deb_build ; tar xzf ../${COQPACKAGE}.tar.gz
-	cp -a debian deb_build/${COQPACKAGE}
-	rm -rf deb_build/${COQPACKAGE}/debian/CVS
-	date > prep-deb
-
-deb: prep-deb
-	cd deb_build/${COQPACKAGE} ; dpkg-buildpackage -rfakeroot -uc -us 2>&1 | tee ../../deb.log
-	(lintian deb_build/${COQDEBCHANGES} | tee lintian.log) || true
-
-deb-sign: prep-deb
-	cd deb_build/${COQPACKAGE} ; dpkg-buildpackage -rfakeroot 2>&1 | tee ../../deb.log
-	(lintian deb_build/${COQDEBCHANGES} | tee lintian.log) || true
+MACOSXPKG=coq-$(VERSION).pkg
+MACOSXDMG=coq-$(VERSION)-macosx.dmg
 
 macosx:
 	# Builds the /usr/local/bin image
@@ -389,29 +368,118 @@ macosx:
 
 macosx-pkg:
 	# Builds the info file
-	sed -e "s/VERSION/${VERSION}/g" MacOS-X/coq.info.template > MacOS-X/coq-${VERSION}.info
+	sed -e "s/VERSION/$(VERSION)/g" MacOS-X/coq.info.template > MacOS-X/coq-$(VERSION).info
 	# Builds the resources files
 	rm -rf MacOS-X/Resources
 	mkdir MacOS-X/Resources
-	sed -e "s/VERSION/${VERSION}/g" MacOS-X/Licence.rtf.template > MacOS-X/Resources/License.rtf
-	sed -e "s/VERSION/${VERSION}/g" MacOS-X/Welcome.rtf.template > MacOS-X/Resources/Welcome.rtf
+	sed -e "s/VERSION/$(VERSION)/g" MacOS-X/Licence.rtf.template > MacOS-X/Resources/License.rtf
+	sed -e "s/VERSION/$(VERSION)/g" MacOS-X/Welcome.rtf.template > MacOS-X/Resources/Welcome.rtf
 	cp MacOS-X/ReadMe.rtf.template MacOS-X/Resources/ReadMe.rtf
 	# Builds the pkg file
-	package MacOS-X/buildroot MacOS-X/coq-${VERSION}.info -r MacOS-X/Resources
+	package MacOS-X/buildroot MacOS-X/coq-$(VERSION).info -r MacOS-X/Resources
+
 
 macosx-dmg:
-	rm -f coq-${VERSION}-macosx.dmg
+	rm -f $(MACOSXDMG)
 	# We successively :
 	# - create the dmg file
 	# - bind it to a device /dev/diskXs2 (name)
 	# - create the file system and name it "Coq X.X"
 	# - unbind the device to mount the image on /Volumes
 	# - copy the package
-	(export size=`du -s coq-${VERSION}.pkg | cut -dc -f 1`;\
-	hdiutil create -sectors `expr $$size + 1000` coq-${VERSION}-macosx.dmg;\
-	export name=`hdid -nomount coq-${VERSION}-macosx.dmg | tail -1 | cut -d" " -f 1`;\
-	newfs_hfs -v "Coq ${VERSION}" $$name;\
-	hdiutil eject $$name; hdid coq-${VERSION}-macosx.dmg;\
-	mkdir "/Volumes/Coq ${VERSION}/coq-${VERSION}.pkg";\
-	ditto -rsrcFork -v coq-${VERSION}.pkg "/Volumes/Coq ${VERSION}/coq-${VERSION}.pkg")
+	(export size=`du -s $(MACOSXPKG) | cut -dc -f 1`;\
+	hdiutil create -sectors `expr $$size + 1000` $(MACOSXDMG);\
+	export name=`hdid -nomount $(MACOSXDMG) | tail -1 | cut -d" " -f 1`;\
+	newfs_hfs -v "Coq $(VERSION)" $$name;\
+	hdiutil eject $$name; hdid $(MACOSXDMG);\
+	mkdir "/Volumes/Coq $(VERSION)/coq-$(VERSION).pkg";\
+	ditto -rsrcFork -v $(MACOSXPKG) "/Volumes/Coq $(VERSION)/$(MACOSXPKG)")
+
+
+###################################################################
+# contribs and patches
+#
+contrib-tag:
+	echo -n "Tagging the contrib with version number $(CVSTAG)...";\
+	cvs rtag -F $(CVSTAG) contrib
+	@echo done
+
+contrib-tar-gz:
+	- rm -rf contrib-$(VERSION)
+	@echo -n Exporting a fresh copy of the contribs...
+	cvs export -d contrib-$(VERSION) -r $(CVSTAG) contrib
+	@echo -n Removing the maintenance files ...
+	@rm -rf contrib-$(VERSION)/*/*/bench.log
+	@rm -rf contrib-$(VERSION)/Lyon/PROGRAMS
+	@find contrib-$(VERSION) -name ".cvsignore" -exec rm {} \;
+	@echo done
+	- rm contrib-$(VERSION).tar.gz
+	@echo -n Building the tar.gz contrib package
+	@tar cvf contrib-$(VERSION).tar contrib-$(VERSION)
+	@gzip --best contrib-$(VERSION).tar
+	@echo done
+
+
+patch:
+	@echo ******** ATTENTION, plante sur pc-linux, essayez pauillac ******
+	$(CP) $(FTPDIR)/V$(PREVIOUSVERSION)/coq-$(PREVIOUSVERSION).tar.gz .
+	rm -rf coq-$(PREVIOUSVERSION)
+	gunzip -c coq-$(PREVIOUSVERSION).tar.gz | tar x
+	rm -rf $(COQPACKAGE)
+	gunzip -c $(TARGZ) | tar x
+	diff -rc coq-$(PREVIOUSVERSION) $(COQPACKAGE) > patch-$(VERSION)-$(PREVIOUSVERSION)
+	gzip --best patch-$(VERSION)-$(PREVIOUSVERSION)
+
+###################################################################
+# Installation in the ftp repository
+#
+
+ftp-install: prep-ftp-install
+	$(CP) $(COQPACKAGE)/CHANGES $(FTPVDIR)/
+	$(CP) $(COQPACKAGE)/README $(FTPVDIR)/
+	$(CP) $(COQPACKAGE)/README.win $(FTPVDIR)/
+	$(CP) $(COQPACKAGE)/README.macosx $(FTVPDIR)/
+	$(CP) $(TARGZ) $(FTPVDIR)/
+	$(CP) $(COQPACKAGE)-*.tar.gz $(FTPVDIR)/
+	$(CP) $(COQRPMPACKAGE).*.rpm $(FTPVDIR)/
+
+# prep-ftp-install: $(FTPDIR)/V$(VERSION)
+prep-ftp-install: 
+	- $(SERVEREXEC) mkdir -m g+w $(FTPDIR)/V$(VERSION)
+
+final-ftp-install:
+	$(SERVEREXEC) "'(cd $(FTPDIR); rm -f current;ln -sf V$(VERSION) current)'"
+
+tar-gz-ftp-install: prep-ftp-install
+	chmod g+w $(TARGZ)
+	$(CP) $(TARGZ) $(FTPVDIR)/
+
+src-rpm-ftp-install: prep-ftp-install
+	chmod g+w $(COQSRCRPM)
+	$(CP) $(COQSRCRPM) $(FTPVDIR)/
+
+arch-rpm-ftp-install: prep-ftp-install
+	chmod g+w $(COQRPM)
+	$(CP) $(COQRPM) $(FTPVDIR)/
+
+arch-tar-gz-ftp-install: prep-ftp-install
+	chmod g+w $(ARCHTARGZ)
+	$(CP) $(ARCHTARGZ) $(FTPVDIR)/
+
+contrib-ftp-install: prep-ftp-install
+	chmod g+w contrib-$(VERSION).tar.gz
+	$(CP) contrib-$(VERSION).tar.gz $(FTPVDIR)/
+
+patch-ftp-install: prep-ftp-install
+	chmod g+w patch-$(VERSION)-$(PREVIOUSVERSION).gz
+	$(CP) patch-$(VERSION)-$(PREVIOUSVERSION).gz $(FTPVDIR)/
+
+###################################################################
+# Special targets
+#
+
+#clean::
+
+cleanall:: clean
+	rm -f config.distrib
 
diff --git a/distrib/RELEASE b/distrib/RELEASE
index 0ef0b09fa5..11b795db21 100644
--- a/distrib/RELEASE
+++ b/distrib/RELEASE
@@ -43,7 +43,7 @@ A1) VÉRIFICATIONS
 
   Dans le cas simple d'une recompilation sur une autre architecture,
 sauter A3. Sauter aussi A4 s'il est possible de mettre le fichier
-coq-6.2.5.tar.gz à la main dans distrib.
+coq-X.Y.Z.tar.gz à la main dans distrib.
 
 A2) CONFIGURATION DES PARAMETRES DE LA DISTRIBUTION
 
@@ -62,7 +62,8 @@ A3) ESTAMPILLAGE DE L'ARCHIVE
 
      make tag
 
-  pour poser le tag V6-2-5 à l'archive V6-2 (on suppose que le numéro de version donné dans configure.distrib est V6.2.5).
+  pour poser le tag V'X'-Y-Z à l'archive V'X' (on suppose que le numéro
+  de version donné dans configure.distrib est V'X'.Y.Z).
 
   La commande "make tag" peut être refaite plusieurs fois auquel cas
 l'ancienne marque est supprimée avant d'être remise à la nouvelle
@@ -74,7 +75,7 @@ l'archive faire "cvs tag -F V6-2-5 nom_du_fichier".
 
 A4) CREATION DU PACKAGE SOURCE
 
-  Créer le coq-6.2.5.tar.gz des sources à partir d'un extrait tout
+  Créer le coq-X.Y.Z.tar.gz des sources à partir d'un extrait tout
 frais (obtenu par cvs export) de l'archive avec
 
      make tar-gz
@@ -96,13 +97,13 @@ A5a) Création d'un package binaire tar.gz
       make arch-tar-gz
 
   dans le répertoire distrib sous l'architecture ARCH avec le système SYS
-crée un fichier coq-6.2.5-SYS-ARCH.tar.gz (ex : coq-6.2.5-alpha-OSF1.tar.gz).
+crée un fichier coq-X.Y.Z-SYS-ARCH.tar.gz (ex : coq-6.2.5-alpha-OSF1.tar.gz).
 
   Pour compiler sur plusieurs machines en parallèle, il faut des
 répertoires "distrib" distincts pour que les compilations ne se
 téléscopent pas. Sur une 2ème machine dans un autre répertoire
 "distrib", refaire "make tar-gz" en interrompant la check-list (ou
-simplement copier le coq-6.2.5.tar.gz déjà fait) puis "make arch-tar-gz".
+simplement copier le coq-X.Y.Z.tar.gz déjà fait) puis "make arch-tar-gz".
 
   Pour l'installation sous ftp voir A7.
 
@@ -114,7 +115,7 @@ A5b) Création du source rpm et du premier package rpm
      make rpm
 
   dans le répertoire distrib sous l'architecture ARCH crée un package
-source coq-6.2.5-1.src.rpm et un package binaire coq-6.2.5-1.ARCH.rpm
+source coq-X.Y.Z-1.src.rpm et un package binaire coq-X.Y.Z-1.ARCH.rpm
 (ex : coq-6.2.5-1.i386.rpm).
 
   Remarques : 1) Les packages Intel s'appellent i386 même si
@@ -133,7 +134,16 @@ A5c) Création d'un second package rpm à partir des sources rpm
 
   Pour l'installation sous ftp voir A7.
 
-A5d) Création du package debian
+A5d) Création d'un package coq-ide
+
+  Faire un
+
+     make rpm-ide
+
+  pour produire un package source coqide-X-Y-Z-1.src.rpm et un package
+  bianire coqide-X-Y-Z-1.ARCH.rpm.
+
+A5e) Création du package debian
 
   Faire un
 
@@ -144,7 +154,7 @@ A5d) Création du package debian
   binaire sur toutes les architectures : ce sera fait par les machines
   de Debian dès que le paquet source leur sera fourni.
 
-A5e) Création du package windows
+A5f) Création du package windows
 
   Habituellement fait sur jurancon.inria.fr, sous Windows NT, avec la
   version Win32 de ocaml (pas la version cygwin car elle produit un
@@ -160,7 +170,7 @@ A5e) Création du package windows
 
   Envoyer ensuite l'archive par ftp dans
 
-    pauillac:/net/pauillac/infosystems/ftp/coq/coq/V6.2.5
+    pauillac:/net/pauillac/infosystems/ftp/coq/coq/V'X'.Y.Z
 
 A6) CREATION DU FICHIER DE PATCH (attention ne marche pas sur DEC je crois)
 
@@ -183,7 +193,7 @@ A7) INSTALLATION SOUS FTP
 
    make ftp-install # Avec les droits du groupe coq
 
-   - crée le dossier /net/pauillac/infosystems/ftp/coq/coq/V6.2.5, le
+   - crée le dossier /net/pauillac/infosystems/ftp/coq/coq/V'X'.Y.Z, le
    lie symboliquement à /net/pauillac/infosystems/ftp/coq/coq/current.
 
    - installe sous ftp tous les fichiers tar.gz ou .rpm du répertoire
diff --git a/distrib/check-list b/distrib/check-list
index 8e277fef52..be39bc665d 100755
--- a/distrib/check-list
+++ b/distrib/check-list
@@ -11,7 +11,7 @@ COQPACKAGE=coq-$VERSION
 CONFIGFILE=$COQPACKAGE/configure
 
 version=`grep "^VERSION=" $CONFIGFILE | sed -e 's/^VERSION=\(.*\)/\1/'`
-versionsi=`grep "^VERSIONSI=" $CONFIGFILE | sed -e 's/^VERSIONSI=\(.*\)/\1/'`
+#versionsi=`grep "^VERSIONSI=" $CONFIGFILE | sed -e 's/^VERSIONSI=\(.*\)/\1/'`
 coqdate=`grep "^DATE=" $CONFIGFILE | sed -e 's/^DATE=\(.*\)/\1/'`
 
 echo "According to the configure file of the archive to be released"
@@ -24,9 +24,9 @@ echo "Comparing datas with expected ones"
 if [ ! "$version" = "$VERSION" ]; then
 	 echo "Inconsistent version number";exit
 fi
-if [ ! "$versionsi" = "$VERSIONSI" ]; then
-	echo "Inconsistent SearchIsos version number";exit
-fi
+#if [ ! "$versionsi" = "$VERSIONSI" ]; then
+#	echo "Inconsistent SearchIsos version number";exit
+#fi
 if [ ! "$date" = "$DATE" ]; then
 	echo "Inconsistent date release";exit
 fi
@@ -75,8 +75,8 @@ echo -n " is that OK? "
 read a
 if [ "$a" != 'y' -a "$a" != 'Y' ]; then echo Aborting; exit 1; fi
 
-versionspec1=`grep "^Version: " ./RH/coq.spec.tpl | sed -e 's!^Version: \(.*\)!\1!'`
-versionspec2=`grep "^Source: " ./RH/coq.spec.tpl | sed -e 's!.*coq-\(.*\)\.tar\.gz.*!\1!'`
+versionspec1=`sed -n -e 's!^Version: \(.*\)!\1!p' ./RH/coq.spec`
+versionspec2=`sed -n -e 's!.*coq-\(.*\)\.tar\.gz.*!\1!' ./RH/coq.spec`
 if [ "$versionspec1" = "$version" -a "$versionspec2" = "$version" ];
 then echo "Version number in coq.spec seems OK ($versionspec1)";
 else
diff --git a/distrib/configure.distrib b/distrib/configure.distrib
index ac52c65b22..bd4faf442e 100755
--- a/distrib/configure.distrib
+++ b/distrib/configure.distrib
@@ -6,12 +6,13 @@
 # 
 ####################################
 #
-#  Default values comes from ../configure which is probably consistent with the archive
+#  Default values comes from ../configure which is probably consistent
+#  with the archive
 #
 
-VERSION=`grep "^VERSION=" ../configure | sed -e 's/^VERSION=\(.*\)/\1/'`
-VERSIONSI=`grep "^VERSIONSI=" ../configure | sed -e 's/^VERSIONSI=\(.*\)/\1/'`
-DATE=`grep "^DATE=" ../configure | sed -e 's/^DATE=\(.*\)/\1/'`
+VERSION=`sed -n -e 's/^VERSION=\(.*\)/\1/p' ../configure`
+#VERSIONSI=`sed -n -e 's/^VERSIONSI=\(.*\)/\1/p' ../configure`
+DATE=`sed -n -e 's/^DATE=\(.*\)/\1/p' ../configure`
 RELEASENUM=1
 DISTRIBDIR=`pwd`
 
@@ -23,32 +24,33 @@ echo Default values are taken from ../configure
 echo ------------------------------------------
 
 # Determine the release number
-echo -n "What is the version number of the current release [$VERSION]? "
+echo -n "Version number of the current release [$VERSION]? "
 read ANSWER
 case $ANSWER in
  "") true;;
  *) VERSION=$ANSWER;
 esac
 
-DASHEDVERSION=V`echo $VERSION | sed -e 's/\./-/g'`
-#MAJORVERSION=V`echo $VERSION | sed -e 's/^\([0-9]\)\.[0-9].*/\1/'`
-MAJORVERSION=V7
-MAINNUMBER=`echo $VERSION | sed -e 's/\(.*\)\.[0-9]*$/\1/'`
-LASTNUMBER=`echo $VERSION | sed -e 's/.*\.\([0-9]*\)$/\1/'`
-if [ "$LASTNUMBER" = "0" ]; then
-        LASTNUMBER=`echo $MAINNUMBER | sed -e 's/.*\.\([0-9]*\)$/\1/g'`
-	MAINNUMBER=`echo $MAINNUMBER | sed -e 's/\(.*\)\.[0-9]*$/\1/'`
-fi
+# The main number of the release
+MAINNUMBER=`echo $VERSION | sed -e 's/^\([0-9]\+*\)\.[0-9]\+.*$/\1/'`
+# The minor number
+LASTNUMBER=`echo $VERSION | sed -e 's/^[0-9]\+\.\([0-9]\+\).*$/\1/'`
+# The release level: alpha, beta, etc.
+LEVEL=`echo $VERSION | sed -e 's/^[0-9]\+\.[0-9]\+\(.*\)$/\1/'`
+
+MAJORVERSION=V$MAINNUMBER
+CVSMODULE=V7
+CVSTAG=V`echo $VERSION | sed -e 's/\./-/g'`
 if [ "$LASTNUMBER" = "0" ]; then
-        LASTNUMBER=`echo $MAINNUMBER | sed -e 's/.*\.\([0-9]*\)$/\1/g'`
-	MAINNUMBER=`echo $MAINNUMBER | sed -e 's/\(.*\)\.[0-9]*$/\1/'`
+    PREVIOUSMAINNUMBER=`expr $MAINNUMBER - 1`
+    PREVIOUSVERSION=$PREVIOUSMAINNUMBER.99
+else
+    PREVIOUSLASTNUMBER=`expr $LASTNUMBER - 1`
+    PREVIOUSVERSION=$MAINNUMBER.$PREVIOUSLASTNUMBER
 fi
-PREVIOUSLASTNUMBER=`expr $LASTNUMBER - 1`
-PREVIOUSVERSION=$MAINNUMBER.$PREVIOUSLASTNUMBER
 
 # Determine the previous release number
-echo -n "What is the version number of the previous release "
-echo -n "(for the patch file) [$PREVIOUSVERSION]? "
+echo -n "Version number of the previous release (for the patch file) [$PREVIOUSVERSION]? "
 read ANSWER
 case $ANSWER in
  "") true;;
@@ -57,15 +59,15 @@ esac
 
 
 # Determine the searchisos version number
-echo -n "What is the version number of the current SearchIsos release [$VERSIONSI]? "
-read ANSWER
-case $ANSWER in
- "") true;;
- *) VERSIONSI=$ANSWER;;
-esac
+#echo -n "What is the version number of the current SearchIsos release [$VERSIONSI]? "
+#read ANSWER
+#case $ANSWER in
+# "") true;;
+# *) VERSIONSI=$ANSWER;;
+#esac
 
 # Determine the date of the release
-echo -n "What is the date of the current release [$DATE]? "
+echo -n "Date of the current release [$DATE]? "
 read ANSWER
 case $ANSWER in
  "") true;;
@@ -73,21 +75,21 @@ case $ANSWER in
 esac
 
 # Determine the rpm release number
-echo -n "What is the release number for the RPM packages [1]? "
+echo -n "Release number for the RPM packages [$RELEASENUM]? "
 read ANSWER
 case $ANSWER in
  "") true;;
  *) RELEASENUM=$ANSWER;;
 esac
 
-echo VERSION=$VERSION > config.distrib
-echo VERSIONSI=$VERSIONSI >> config.distrib
-echo PREVIOUSVERSION=$PREVIOUSVERSION >> config.distrib
+echo CVSMODULE=$CVSMODULE > config.distrib
+echo CVSTAG=$CVSTAG >> config.distrib
 echo DISTRIBDIR=$DISTRIBDIR >> config.distrib
-echo DASHEDVERSION=$DASHEDVERSION >> config.distrib
-echo MAJORVERSION=$MAJORVERSION >> config.distrib
+echo VERSION=$VERSION >> config.distrib
 echo RELEASENUM=$RELEASENUM >> config.distrib
 echo ARCH=$ARCH >> config.distrib
+echo PREVIOUSVERSION=$PREVIOUSVERSION >> config.distrib
+#echo VERSIONSI=$VERSIONSI >> config.distrib
 chmod +x config.distrib
 
 # $Id$
diff --git a/doc/syntax-v8.tex b/doc/syntax-v8.tex
index 53e191e98f..9eb3c7a636 100644
--- a/doc/syntax-v8.tex
+++ b/doc/syntax-v8.tex
@@ -1154,7 +1154,7 @@ $$
 \nlsep \TERM{Proof}~\KWD{with}~\NT{tactic}
 \nlsep \TERM{Abort}~\OPT{\TERM{All}}
 \nlsep \TERM{Abort}~\NT{ident}
-\nlsep \TERM{Existential}~\NT{num}~\NT{constr-body}
+\nlsep \TERM{Existential}~\NT{num}~\KWD{:=}~\NT{constr-body}
 \nlsep \TERM{Qed}
 \nlsep \TERM{Save}~\OPTGR{\NT{thm-token}~\NT{ident}}
 \nlsep \TERM{Defined}~\OPT{\NT{ident}}
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 60e6657d54..e28065afd8 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1493,13 +1493,13 @@ let rec extern inctx scopes vars r =
 
   | RLetTuple (loc,nal,(na,typopt),tm,b) ->
       CLetTuple (loc,nal,
-        (na,option_app (extern_type scopes (add_vname vars na)) typopt),
+        (Some na,option_app (extern_type scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars tm,
         extern false scopes (List.fold_left add_vname vars nal) b)
 
   | RIf (loc,c,(na,typopt),b1,b2) ->
       CIf (loc,sub_extern false scopes vars c,
-        (na,option_app (extern_type scopes (add_vname vars na)) typopt),
+        (Some na,option_app (extern_type scopes (add_vname vars na)) typopt),
         sub_extern false scopes vars b1, sub_extern false scopes vars b2)
 
   | RRec (loc,fk,idv,tyv,bv) ->
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index dfa6a1b94e..c6a819d440 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -757,13 +757,12 @@ let internalise sigma env allow_soapp lvar c =
 	  | RApp (loc', f', args') -> RApp (join_loc loc' loc, f',args'@args)
 	  | _ -> RApp (loc, c, args))
     | CCases (loc, (po,rtnpo), tms, eqns) ->
-        let tms,rtnids = List.fold_right (fun (tm,indnalo) (inds,ids) ->
-          let tm' = intern env tm in
-	  let typ,ids = intern_return_type env indnalo tm' ids in
-	  (tm',ref typ)::inds,ids)
-	  tms ([],ids) in
-        let rtnpo =
-          option_app (intern_type (rtnids,tmp_scope,scopes)) rtnpo in
+        let tms,env' = List.fold_right
+          (fun citm (inds,env) ->
+	    let (tm,ind),nal = intern_case_item env citm in
+	    (tm,ref ind)::inds,List.fold_left (push_name_env lvar) env nal)
+	  tms ([],env) in
+        let rtnpo = option_app (intern_type env') rtnpo in
 	RCases (loc, (option_app (intern_type env) po, ref rtnpo), tms,
 		List.map (intern_eqn (List.length tms) env) eqns)
     | COrderedCase (loc, tag, po, c, cl) ->
@@ -773,15 +772,17 @@ let internalise sigma env allow_soapp lvar c =
 		  Array.of_list (List.map (intern env) cl),ref None)
     | CLetTuple (loc, nal, (na,po), b, c) ->
 	let env' = reset_tmp_scope env in
-        RLetTuple (loc, nal,
-           (na, option_app (intern_type (push_name_env lvar env' na)) po),
-           intern env' b,
-	   intern (List.fold_left (push_name_env lvar) env nal) c)
+        let ((b',(na',_)),ids) = intern_case_item env' (b,(na,None)) in
+        let env'' = List.fold_left (push_name_env lvar) env ids in
+        let p' = option_app (intern_type env'') po in
+        RLetTuple (loc, nal, (na', p'), b',
+                   intern (List.fold_left (push_name_env lvar) env nal) c)
     | CIf (loc, c, (na,po), b1, b2) ->
-	let env = reset_tmp_scope env in
-        RIf (loc, intern env c,
-           (na, option_app (intern_type (push_name_env lvar env na)) po),
-           intern env b1, intern env b2)
+	let env' = reset_tmp_scope env in
+        let ((c',(na',_)),ids) = intern_case_item env' (c,(na,None)) in
+        let env'' = List.fold_left (push_name_env lvar) env ids in
+        let p' = option_app (intern_type env'') po in
+        RIf (loc, c', (na', p'), intern env b1, intern env b2)
     | CHole loc -> 
 	RHole (loc, QuestionMark)
     | CPatVar (loc, n) when allow_soapp ->
@@ -823,31 +824,31 @@ let internalise sigma env allow_soapp lvar c =
 	let env_ids = List.fold_right Idset.add eqn_ids ids in
 	(loc, eqn_ids,pl,intern (env_ids,tmp_scope,scopes) rhs)
 
-  and intern_return_type (vars,_,scopes as env) (na,t) tm ids =
+  and intern_case_item (vars,_,scopes as env) (tm,(na,t)) =
+    let tm' = intern env tm in
     let ids,typ = match t with
     | Some t -> 
 	let tids = names_of_cases_indtype t in
 	let tids = List.fold_right Idset.add tids Idset.empty in
 	let t = intern_type (tids,None,scopes) t in
 	begin match t with
-	  | RRef (loc,IndRef ind) -> ids,Some (loc,ind,[])
+	  | RRef (loc,IndRef ind) -> [],Some (loc,ind,[])
 	  | RApp (loc,RRef (_,IndRef ind),l) ->
 	      let nal = List.map (function
 		| RHole _ -> Anonymous
 		| RVar (_,id) -> Name id
 		| c ->
 		    user_err_loc (loc_of_rawconstr c,"",str "Not a name")) l in
-	      List.fold_right (name_fold Idset.add) nal ids,
-	      Some (loc,ind,nal)
+	      nal, Some (loc,ind,nal)
 	  | _ -> error_bad_inductive_type (loc_of_rawconstr t)
 	end
     | None -> 
-	ids, None in
-    let na = match tm, na with
+	[], None in
+    let na = match tm', na with
       | RVar (_,id), None when Idset.mem id vars & not !Options.v7 -> Name id
       | _, None -> Anonymous
       | _, Some na -> na in
-    (na,typ), name_fold Idset.add na ids
+    (tm',(na,typ)), na::ids
 
   and iterate_prod loc2 env ty body = function
     | (loc1,na)::nal ->
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index cc9488a3e3..7dda9a3175 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -347,9 +347,9 @@ type constr_expr =
       (loc * cases_pattern_expr list * constr_expr) list
   | COrderedCase of loc * case_style * constr_expr option * constr_expr
       * constr_expr list
-  | CLetTuple of loc * name list * (name * constr_expr option) *
+  | CLetTuple of loc * name list * (name option * constr_expr option) *
       constr_expr * constr_expr
-  | CIf of loc * constr_expr * (name * constr_expr option)
+  | CIf of loc * constr_expr * (name option * constr_expr option)
       * constr_expr * constr_expr
   | CHole of loc
   | CPatVar of loc * (bool * patvar)
@@ -510,13 +510,13 @@ let map_constr_expr_with_binders f g e = function
          List.map (fun (tm,x) -> (f e tm,x)) a,bl)
   | COrderedCase (loc,s,po,a,bl) ->
       COrderedCase (loc,s,option_app (f e) po,f e a,List.map (f e) bl)
-  | CLetTuple (loc,nal,(na,po),b,c) ->
+  | CLetTuple (loc,nal,(ona,po),b,c) ->
       let e' = List.fold_right (name_fold g) nal e in
-      let e'' = name_fold g na e in
-      CLetTuple (loc,nal,(na,option_app (f e'') po),f e b,f e' c)
-  | CIf (loc,c,(na,po),b1,b2) ->
-      let e' = name_fold g na e in
-      CIf (loc,f e c,(na,option_app (f e') po),f e b1,f e b2)
+      let e'' = option_fold_right (name_fold g) ona e in
+      CLetTuple (loc,nal,(ona,option_app (f e'') po),f e b,f e' c)
+  | CIf (loc,c,(ona,po),b1,b2) ->
+      let e' = option_fold_right (name_fold g) ona e in
+      CIf (loc,f e c,(ona,option_app (f e') po),f e b1,f e b2)
   | CFix (loc,id,dl) ->
       CFix (loc,id,List.map (fun (id,n,t,d) -> (id,n,f e t,f e d)) dl)
   | CCoFix (loc,id,dl) ->
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 65beaa511e..c6be360284 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -93,9 +93,9 @@ type constr_expr =
       (loc * cases_pattern_expr list * constr_expr) list
   | COrderedCase of loc * case_style * constr_expr option * constr_expr
       * constr_expr list
-  | CLetTuple of loc * name list * (name * constr_expr option) *
+  | CLetTuple of loc * name list * (name option * constr_expr option) *
       constr_expr * constr_expr
-  | CIf of loc * constr_expr * (name * constr_expr option)
+  | CIf of loc * constr_expr * (name option * constr_expr option)
       * constr_expr * constr_expr
   | CHole of loc
   | CPatVar of loc * (bool * patvar)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 8fee8481d7..33eae08213 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -115,9 +115,11 @@ and merge_with env mtb with_decl =
 		let _ = subst_modtype (map_msid msid (MPself msid)) mtb in
 		  ()
 	      with
-		  Assert_failure _ -> error_circular_with_module id
+		  Failure _ -> error_circular_with_module id
 	    end;
-	    let cst = check_subtypes env' mtb old.msb_modtype in
+	    let cst =
+              try check_subtypes env' mtb old.msb_modtype
+              with Failure _ -> error_with_incorrect (label_of_id id) in
 	    let equiv = 
  	      match old.msb_equiv with
 		| None -> Some mp
@@ -213,7 +215,10 @@ and translate_module env is_definition me =
 	    | None -> mtb1, None, Constraint.empty
 	    | Some mte -> 
 		let mtb2 = translate_modtype env mte in
-		  mtb2, Some mtb2, check_subtypes env mtb1 mtb2
+                let cst =
+                  try check_subtypes env mtb1 mtb2
+                  with Failure _ -> error "not subtype" in
+		mtb2, Some mtb2, cst
 	in
 	  { mod_type = mtb;
 	    mod_user_type = mod_user_type;
@@ -237,7 +242,10 @@ and translate_mexpr env mexpr = match mexpr with
       let ftb = scrape_modtype env ftb in
       let farg_id, farg_b, fbody_b = destr_functor ftb in
       let meb,mtb = translate_mexpr env mexpr in
-      let cst = check_subtypes env mtb farg_b in
+      let cst =
+        try check_subtypes env mtb farg_b
+        with Failure _ ->
+          error "" in
       let mp = 
 	try
 	  path_of_mexpr mexpr 
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 7459dcad8d..569580bfb1 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -125,12 +125,12 @@ let rec check_modpath_equiv env mp1 mp2 =
 let rec subst_modtype sub = function
   | MTBident ln -> MTBident (subst_kn sub ln)
   | MTBfunsig (arg_id, arg_b, body_b) ->
-      assert (not (occur_mbid arg_id sub));
+      if occur_mbid arg_id sub then failwith "capture";
       MTBfunsig (arg_id, 
 		 subst_modtype sub arg_b, 
 		 subst_modtype sub body_b)
   | MTBsig (sid1, msb) -> 
-      assert (not (occur_msid sid1 sub));
+      if occur_msid sid1 sub then failwith "capture";
       MTBsig (sid1, subst_signature sub msb)
 
 and subst_signature sub sign = 
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 6b0931a9e3..50aeaf3473 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -244,4 +244,3 @@ and check_modtypes cst env mtb1 mtb2 equiv =
 	  
 let check_subtypes env sup super = 
   check_modtypes Constraint.empty env sup super false
-
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml
index 25333b6848..533919b676 100644
--- a/parsing/egrammar.ml
+++ b/parsing/egrammar.ml
@@ -230,11 +230,11 @@ let subst_constr_expr a loc subs =
   | COrderedCase (_,s,po,a,bl) ->
       COrderedCase (loc,s,option_app subst po,subst a,List.map subst bl)
   | CLetTuple (_,nal,(na,po),a,b) ->
-      let na = name_app (subst_id subs) na in
+      let na = option_app (name_app (subst_id subs)) na in
       let nal = List.map (name_app (subst_id subs)) nal in
       CLetTuple (loc,nal,(na,option_app subst po),subst a,subst b)
   | CIf (_,c,(na,po),b1,b2) ->
-      let na = name_app (subst_id subs) na in
+      let na = option_app (name_app (subst_id subs)) na in
       CIf (loc,subst c,(na,option_app subst po),subst b1,subst b2)
   | CFix (_,id,dl) ->
       CFix (loc,id,List.map (fun (id,n,t,d) -> (id,n,subst t,subst d)) dl)
diff --git a/parsing/g_constrnew.ml4 b/parsing/g_constrnew.ml4
index 4cf3f25ab4..101c29d31f 100644
--- a/parsing/g_constrnew.ml4
+++ b/parsing/g_constrnew.ml4
@@ -275,10 +275,10 @@ GEXTEND Gram
     [ [ "return"; ty = operconstr LEVEL "100" -> ty ] ]
   ;
   return_type:
-    [ [ a = OPT [ na = ["as"; id=name -> snd id | -> Names.Anonymous];
-              ty = case_type -> (na,ty) ] -> 
+    [ [ a = OPT [ na = OPT["as"; id=name -> snd id];
+                  ty = case_type -> (na,ty) ] -> 
         match a with 
-          | None -> Names.Anonymous, None
+          | None -> None, None
           | Some (na,t) -> (na, Some t)
     ] ]
   ;
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index b108ab4b42..4cdf0bc35c 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -16,6 +16,8 @@ open Tacexpr
 open Rawterm
 open Genarg
 
+let compute = Cbv all_flags
+
 let tactic_kw =
   [ "->"; "<-" ]
 let _ = 
@@ -231,7 +233,7 @@ GEXTEND Gram
       | IDENT "simpl"; po = OPT pattern_occ -> Simpl po
       | IDENT "cbv"; s = LIST1 red_flag -> Cbv (make_red_flag s)
       | IDENT "lazy"; s = LIST1 red_flag -> Lazy (make_red_flag s)
-      | IDENT "compute" -> Cbv (make_red_flag [FBeta;FIota;FDeltaBut [];FZeta])
+      | IDENT "compute" -> compute
       | IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
       | IDENT "fold"; cl = LIST1 constr -> Fold cl
       | IDENT "pattern"; pl = LIST1 pattern_occ SEP","-> Pattern pl ] ]
@@ -243,7 +245,7 @@ GEXTEND Gram
       | IDENT "simpl"; po = OPT pattern_occ -> Simpl po
       | IDENT "cbv"; s = LIST1 red_flag -> Cbv (make_red_flag s)
       | IDENT "lazy"; s = LIST1 red_flag -> Lazy (make_red_flag s)
-      | IDENT "compute" -> Cbv (make_red_flag [FBeta;FIota;FDeltaBut [];FZeta])
+      | IDENT "compute" -> compute
       | IDENT "unfold"; ul = LIST1 unfold_occ -> Unfold ul
       | IDENT "fold"; cl = LIST1 constr -> Fold cl
       | IDENT "pattern"; pl = LIST1 pattern_occ -> Pattern pl
diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4
index dadfc18d05..2b3c17b149 100644
--- a/parsing/tacextend.ml4
+++ b/parsing/tacextend.ml4
@@ -159,11 +159,20 @@ let declare_tactic_v7 loc s cl =
       List.iter (Pptactic.declare_extra_tactic_pprule False $se$) $pp$;
     end
   >>
-(*
-let declare_atomic_extend s = 
-  Tacinterp.add_tacdef false
-    [(Names.id_of_string s,dummy_loc),Tacexpr.TacExtend(dummy_loc,s,[])]
-*)
+
+let rec contains_epsilon = function
+  | List0ArgType _ -> true
+  | List1ArgType t -> contains_epsilon t
+  | OptArgType _ -> true
+  | PairArgType(t1,t2) -> contains_epsilon t1 && contains_epsilon t2
+  | ExtraArgType("hintbases") -> true
+  | _ -> false
+let is_atomic =
+  List.for_all
+    (function
+        TacTerm _ -> false
+      | TacNonTerm(_,t,_,_) -> contains_epsilon t)
+
 let declare_tactic loc s cl =
   let (s',cl') = new_tac_ext (s,cl) in
   let pp' = make_printing_rule cl' in
@@ -184,12 +193,19 @@ let declare_tactic loc s cl =
   in
   let hidden = if List.length cl = 1 then List.map hide_tac cl' else [] in
   let se = mlexpr_of_string s in
+  let atomic_tactics =
+    mlexpr_of_list (fun (s,_,_) -> mlexpr_of_string s)
+      (List.filter (fun (_,al,_) -> is_atomic al) cl') in
   <:str_item<
     declare
       open Pcoq;
       declare $list:hidden$ end;
       try
-       Refiner.add_tactic $se'$ (fun [ $list:make_clauses s' cl'$ ])
+        let _=Refiner.add_tactic $se'$ (fun [ $list:make_clauses s' cl'$ ]) in
+        List.iter
+          (fun s -> Tacinterp.add_primitive_tactic s
+              (Tacexpr.TacAtom((0,0),Tacexpr.TacExtend((0,0),s,[]))))
+          $atomic_tactics$
       with e -> Pp.pp (Cerrors.explain_exn e);
       if Options.v7.val then Egrammar.extend_tactic_grammar $se'$ $gl$
       else Egrammar.extend_tactic_grammar $se'$ $gl'$;
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 78425e107a..6442ca9693 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -324,6 +324,9 @@ type 'a raw_red_flag = {
   rConst : 'a list
 }
 
+let all_flags =
+  {rBeta = true; rIota = true; rZeta = true; rDelta = true; rConst = []}
+
 type 'a occurrences = int list * 'a
 
 type ('a,'b) red_expr_gen =
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 651530c94c..869861ccd7 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -117,6 +117,8 @@ type 'a raw_red_flag = {
   rConst : 'a list
 }
 
+val all_flags : 'a raw_red_flag
+
 type 'a occurrences = int list * 'a
 
 type ('a,'b) red_expr_gen =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8a1bbd3cb0..bc9a21ff32 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -242,15 +242,44 @@ let coerce_to_inductive = function
 
 
 (* Table of "pervasives" macros tactics (e.g. auto, simpl, etc.) *)
-let initmactab = ref Gmap.empty
+let atomic_mactab = ref Idmap.empty
+let add_primitive_tactic s tac =
+  let id = id_of_string s in
+  atomic_mactab := Idmap.add id tac !atomic_mactab
 
+let _ =
+  if not !Options.v7 then
+    let nocl = {onhyps=Some[];onconcl=true; concl_occs=[]} in
+    List.iter
+      (fun (s,t) -> add_primitive_tactic s (TacAtom((0,0),t)))
+      [ "red", TacReduce(Red false,nocl);
+        "hnf", TacReduce(Hnf,nocl);
+        "simpl", TacReduce(Simpl None,nocl);
+        "compute", TacReduce(Cbv all_flags,nocl);
+        "intro", TacIntroMove(None,None);
+        "intros", TacIntroPattern [];
+        "assumption", TacAssumption;
+        "cofix", TacCofix None;
+        "trivial", TacTrivial None;
+        "auto", TacAuto(None,None);
+        "left", TacLeft NoBindings;
+        "right", TacRight NoBindings;
+        "split", TacSplit(false,NoBindings);
+        "constructor", TacAnyConstructor None;
+        "reflexivity", TacReflexivity;
+        "symmetry", TacSymmetry nocl
+      ]
+
+let lookup_atomic id = Idmap.find id !atomic_mactab
+let is_atomic id = Idmap.mem id !atomic_mactab
+let is_atomic_kn kn =
+  let (_,_,l) = repr_kn kn in
+  is_atomic (id_of_label l)
 
 (* Summary and Object declaration *)
 let mactab = ref Gmap.empty
 
-let lookup r =
-  try Gmap.find r !mactab
-  with Not_found -> Gmap.find r !initmactab
+let lookup r = Gmap.find r !mactab
 
 let _ =
   let init () = mactab := Gmap.empty in
@@ -404,16 +433,19 @@ let intern_constr_reference strict ist = function
       let loc,qid = qualid_of_reference r in
       RRef (loc,locate_reference qid), if strict then None else Some (CRef r)
 
-let intern_reference strict ist r =
-  try Reference (intern_tac_ref ist r)
-  with Not_found -> 
-  try ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
-  with Not_found ->
-  match r with
-    | Ident (loc,id) when not strict -> Identifier id
-    | _ -> 
-        let (loc,qid) = qualid_of_reference r in
-        error_global_not_found_loc loc qid
+let intern_reference strict ist = function
+  | Ident (loc,id) when is_atomic id -> Tacexp (lookup_atomic id)
+  | r ->
+      (try Reference (intern_tac_ref ist r)
+      with Not_found ->
+        (try
+          ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
+        with Not_found ->
+          (match r with
+            | Ident (loc,id) when not strict -> Identifier id
+            | _ ->
+                let (loc,qid) = qualid_of_reference r in
+                error_global_not_found_loc loc qid)))
 
 let rec intern_intro_pattern lf ist = function
   | IntroOrAndPattern l ->
@@ -2090,7 +2122,7 @@ let (inMD,outMD) =
 (* Adds a definition for tactics in the table *)
 let make_absolute_name (loc,id) =
   let kn = Lib.make_kn id in
-  if Gmap.mem kn !mactab or Gmap.mem kn !initmactab then
+  if Gmap.mem kn !mactab or is_atomic_kn kn then
     user_err_loc (loc,"Tacinterp.add_tacdef",
       str "There is already an Ltac named " ++ pr_id id);
   kn
@@ -2114,12 +2146,6 @@ let add_tacdef isrec tacl =
     (fun (id,_) -> Options.if_verbose msgnl (pr_id id ++ str " is defined"))
     rfun
 
-let add_primitive_tactic s tac =
-  let kn = Lib.make_kn (id_of_string s) in
-(*  Nametab.push_tactic (Until 0) sp kn) defs;*)
-  initmactab := Gmap.add kn tac !initmactab
-
-
 (***************************************************************************)
 (* Other entry points *)
 
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index c287dbbfd4..ce43c9c619 100755
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -12,9 +12,11 @@ open Printf
 open Coqdep_lexer
 open Unix
 
+let (/) = Filename.concat
+
 let file_concat l =
   if l=[] then "<empty>" else
-    List.fold_left Filename.concat (List.hd l) (List.tl l)
+    List.fold_left (/) (List.hd l) (List.tl l)
 
 let stderr = Pervasives.stderr
 let stdout = Pervasives.stdout
@@ -94,7 +96,7 @@ let safe_assoc verbose file k =
 let file_name = function
   | (s,None)     -> file_concat s 
   | (s,Some ".") -> file_concat s
-  | (s,Some d)   -> Filename.concat d (file_concat s)
+  | (s,Some d)   -> d / file_concat s
 
 let traite_fichier_ML md ext =
   try 
@@ -375,7 +377,7 @@ let all_subdirs root_dir log_dir =
 	let f = readdir dirh in
 	if f <> "." && f <> ".." then
 	  let file = dir@[f] in
-          let filename = Filename.concat phys_dir f in
+          let filename = phys_dir/f in
 	  if (stat filename).st_kind = S_DIR then begin
 	    add (filename,file);
 	    traverse filename file
@@ -393,7 +395,7 @@ let usage () =
   exit 1
 
 let add_coqlib_known dir_name f =
-  let complete_name = Filename.concat dir_name f in
+  let complete_name = dir_name/f in
   let lib_name = Filename.basename dir_name in
   match try (stat complete_name).st_kind with _ -> S_BLK with 
     | S_REG -> 
@@ -422,7 +424,7 @@ let coqdep () =
       match (old_dirname,new_dirname) with 
 	| (d, ".") -> d
 	| (None,d) -> Some d
-	| (Some d1,d2) -> Some (Filename.concat d1 d2) 
+	| (Some d1,d2) -> Some (d1/d2) 
     in
     let complete_name = file_name ([name],dirname) in
     match try (stat complete_name).st_kind with _ -> S_BLK with 
@@ -432,7 +434,7 @@ let coqdep () =
              let newdirname = 
                match dirname with 
                  | None -> name
-                 | Some d -> Filename.concat d name 
+                 | Some d -> d/name 
 	     in
 	     try 
 	       while true do treat (Some newdirname) (readdir dir) done
@@ -453,7 +455,7 @@ let coqdep () =
       | _ -> ()
   in 
   let add_known phys_dir log_dir f =
-    let complete_name = Filename.concat phys_dir f in
+    let complete_name = phys_dir/f in
     match try (stat complete_name).st_kind with _ -> S_BLK with 
 	| S_REG ->
 	    if Filename.check_suffix f ".ml" then
@@ -468,7 +470,7 @@ let coqdep () =
 	    else if Filename.check_suffix f ".v" then
 	      let basename = Filename.chop_suffix f ".v" in
               let name = log_dir@[basename] in
-              let file = Filename.concat phys_dir basename in
+              let file = phys_dir/basename in
               let paths = [name;[basename]] in
 	      List.iter
                 (fun n -> safe_addQueue clash_v vKnown (n,file)) paths
@@ -507,11 +509,10 @@ let coqdep () =
   parse (List.tl (Array.to_list Sys.argv));
   List.iter
     (fun (s,_) -> add_coqlib_directory s)
-    (all_subdirs (Filename.concat !coqlib "theories") "Coq");
-  add_coqlib_directory (Filename.concat !coqlib "tactics");
+    (all_subdirs (!coqlib/"theories") "Coq");
   List.iter 
     (fun (s,_) -> add_coqlib_directory s)
-    (all_subdirs (Filename.concat !coqlib "contrib") "Coq");
+    (all_subdirs (!coqlib/"contrib") "Coq");
   mliKnown := !mliKnown @ (List.map (fun (f,_,d) -> (f,d)) !mliAccu);
   mlKnown  := !mlKnown @ (List.map (fun (f,_,d) -> (f,d)) !mlAccu);
   warning_mult ".mli" !mliKnown;
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 95e29fd218..5165abfd5a 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -12,16 +12,18 @@ open Pp
 open System
 open Toplevel
 
+let (/) = Filename.concat
+
 let set_debug () = Options.debug := true
 
 (* Loading of the ressource file.
    rcfile is either $HOME/.coqrc.VERSION, or $HOME/.coqrc if the first one
   does not exist. *)
 
-let rcfile = ref (Filename.concat home ".coqrc")
+let rcfile = ref (home/".coqrc")
 let rcfile_specified = ref false
 let set_rcfile s = rcfile := s; rcfile_specified := true
-let set_rcuser s = rcfile := Filename.concat ("~"^s) ".coqrc"
+let set_rcuser s = rcfile := ("~"^s)/".coqrc"
 
 let load_rc = ref true
 let no_load_rc () = load_rc := false
@@ -77,7 +79,7 @@ let init_load_path () =
       (* variable COQLIB overrides the default library *)
     else getenv_else "COQLIB" Coq_config.coqlib in
   (* first user-contrib *)
-  let user_contrib = Filename.concat coqlib "user-contrib" in
+  let user_contrib = coqlib/"user-contrib" in
   if Sys.file_exists user_contrib then 
     Mltop.add_path user_contrib Nameops.default_root_prefix;
   (* then standard library *)
@@ -85,8 +87,8 @@ let init_load_path () =
     if !Options.v7 then [ "theories7"; "contrib7" ]
     else [ "theories"; "contrib" ] in
   let dirs = 
-    (if !Options.v7 then "states7" else "states") :: dev @ vdirs @ [ "ide" ] in
-  List.iter (fun s -> coq_add_rec_path (Filename.concat coqlib s)) dirs;
+    (if !Options.v7 then "states7" else "states") :: dev @ vdirs in
+  List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs;
   let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
   add_ml_include camlp4;
   (* then current directory *)
@@ -101,13 +103,13 @@ let init_library_roots () =
 
 (* Initialises the Ocaml toplevel before launching it, so that it can
    find the "include" file in the *source* directory *)
-let init_ocaml_path () =
 (* We only assume that the variable COQTOP is set *)
+let init_ocaml_path () =
   let coqtop = getenv_else "COQTOP" Coq_config.coqtop in
   let add_subdir dl = 
-    Mltop.add_ml_dir (List.fold_left Filename.concat coqtop dl) 
+    Mltop.add_ml_dir (List.fold_left (/) coqtop dl) 
   in
   List.iter add_subdir
     [ [ "config" ]; [ "dev" ]; [ "lib" ]; [ "kernel" ]; [ "library" ]; 
       [ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ];
-      [ "tactics" ]; [ "toplevel" ] ]
+      [ "tactics" ]; [ "toplevel" ]; [ "translate" ]; [ "ide" ] ]
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 72ac4f086a..9561d03252 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -137,7 +137,7 @@ let re_exec () =
       if dir <> "." then Filename.concat dir com else com 
     in
     Sys.argv.(0) <- newprog;
-    Unix.handle_unix_error Unix.execvp newprog Sys.argv
+    Unix.handle_unix_error (Unix.execvp newprog) Sys.argv
   end
 
 (*s Parsing of the command line.
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 2b7688f8d3..ade7f0e940 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -46,7 +46,6 @@ let pr_db ctx i =
   with Not_found -> str"UNBOUND_REL_"++int i
 
 let explain_unbound_rel ctx n =
-  let ctx = make_all_name_different ctx in
   let pe = pr_ne_context_of (str "In environment") ctx in
   str"Unbound reference: " ++ pe ++
   str"The reference " ++ int n ++ str " is free"
@@ -56,7 +55,6 @@ let explain_unbound_var ctx v =
   str"No such section variable or assumption : " ++ var
 
 let explain_not_type ctx j =
-  let ctx = make_all_name_different ctx in
   let pe = pr_ne_context_of (str"In environment") ctx in
   let pc,pt = prjudge_env ctx j in
   pe ++ str "the term" ++ brk(1,1) ++ pc ++ spc () ++
@@ -64,7 +62,6 @@ let explain_not_type ctx j =
   str"which should be Set, Prop or Type."
 
 let explain_bad_assumption ctx j =
-  let ctx = make_all_name_different ctx in
   let pe = pr_ne_context_of (str"In environment") ctx in
   let pc,pt = prjudge_env ctx j in
   pe ++ str "cannot declare a variable or hypothesis over the term" ++
@@ -140,7 +137,6 @@ let explain_ill_formed_branch ctx c i actty expty =
   str "which should be" ++ brk(1,1) ++ pe
 
 let explain_generalization ctx (name,var) j =
-  let ctx = make_all_name_different ctx in
   let pe = pr_ne_context_of (str "In environment") ctx in
   let pv = prtype_env ctx var in
   let (pc,pt) = prjudge_env (push_rel_assum (name,var) ctx) j in
@@ -151,7 +147,6 @@ let explain_generalization ctx (name,var) j =
   spc () ++ str"which should be Set, Prop or Type."
 
 let explain_actual_type ctx j pt =
-  let ctx = make_all_name_different ctx in
   let pe = pr_ne_context_of (str "In environment") ctx in
   let (pc,pct) = prjudge_env ctx j in
   let pt = prterm_env ctx pt in
@@ -161,7 +156,6 @@ let explain_actual_type ctx j pt =
   str "while it is expected to have type" ++ brk(1,1) ++ pt
 
 let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl =
-  let ctx = make_all_name_different ctx in
   let randl = Array.to_list randl in
 (*  let pe = pr_ne_context_of (str"in environment") ctx in*)
   let pr,prt = prjudge_env ctx rator in
@@ -184,7 +178,6 @@ let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl =
   str"which should be coercible to" ++ brk(1,1) ++ prterm_env ctx exptyp
 
 let explain_cant_apply_not_functional ctx rator randl =
-  let ctx = make_all_name_different ctx in
   let randl = Array.to_list randl in
 (*  let pe = pr_ne_context_of (str"in environment") ctx in*)
   let pr = prterm_env ctx rator.uj_val in
@@ -204,7 +197,6 @@ let explain_cant_apply_not_functional ctx rator randl =
   str" " ++ v 0 appl
 
 let explain_unexpected_type ctx actual_type expected_type =
-  let ctx = make_all_name_different ctx in
   let pract = prterm_env ctx actual_type in
   let prexp = prterm_env ctx expected_type in
   str"This type is" ++ spc () ++ pract ++ spc () ++ 
@@ -212,7 +204,6 @@ let explain_unexpected_type ctx actual_type expected_type =
   spc () ++ prexp
 
 let explain_not_product ctx c =
-  let ctx = make_all_name_different ctx in
   let pr = prterm_env ctx c in
   str"The type of this term is a product," ++ spc () ++
   str"but it is casted with type" ++
@@ -304,13 +295,13 @@ let explain_ill_typed_rec_body ctx i names vdefj vargs =
   str"recursive definition"  ++ spc () ++ pvd ++ spc () ++
   str "has type" ++ spc () ++ pvdt ++spc () ++ 
   str "it should be" ++ spc () ++ pv 
-
+(*
 let explain_not_inductive ctx c =
   let ctx = make_all_name_different ctx in
   let pc = prterm_env ctx c in
   str"The term" ++ brk(1,1) ++ pc ++ spc () ++
   str "is not an inductive definition"
-
+*)
 let explain_cant_find_case_type ctx c =
   let ctx = make_all_name_different ctx in
   let pe = prterm_env ctx c in
@@ -375,7 +366,9 @@ let explain_wrong_case_info ctx ind ci =
     spc () ++ pc
        
 
-let explain_type_error ctx = function
+let explain_type_error ctx err =
+  let ctx = make_all_name_different ctx in
+  match err with
   | UnboundRel n -> 
       explain_unbound_rel ctx n
   | UnboundVar v -> 
@@ -412,7 +405,9 @@ let explain_type_error ctx = function
   | NotInductive c ->
       explain_not_inductive ctx c
 *)
-let explain_pretype_error ctx = function
+let explain_pretype_error ctx err =
+  let ctx = make_all_name_different ctx in
+  match err with
   | CantFindCaseType c ->
       explain_cant_find_case_type ctx c
   | OccurCheck (n,c) ->
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index cbf9de04f5..602fcf171e 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -317,7 +317,7 @@ let rec coq_switch b =
     | End_of_input -> msgerrnl (mt ()); pp_flush(); exit 0
     | Vernacexpr.Quit -> exit 0
     | e ->
-	msgerrnl (str"Anomaly: toplevel loop. Please report.");
+	msgerrnl (str"Anomaly. Please report.");
 	coq_switch b
 
 let loop () = coq_switch true
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 8a2ce3765b..9a86e3ffa4 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -426,7 +426,8 @@ let pr_return_type pr po = pr_case_type pr po
 
 let pr_simple_return_type pr na po =
   (match na with
-    | Name id -> spc () ++ str "as " ++  pr_id id
+    | Some (Name id) ->
+        spc () ++ str "as " ++  pr_id id
     | _ -> mt ()) ++
   pr_case_type pr po