From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 2 Feb 2006 14:02:18 +0000 (+0000)
Subject: no more multiple configure/Makefile, just one for both ocaml/ and matita/
X-Git-Tag: make_still_working~7681
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7be6aeb94aa8da17732511a4844bd108976f947f;p=helm.git

no more multiple configure/Makefile, just one for both ocaml/ and matita/
---

diff --git a/helm/Makefile b/helm/Makefile
index 2eb93cd41..62b41c430 100644
--- a/helm/Makefile
+++ b/helm/Makefile
@@ -1,6 +1,6 @@
 
 BASENAME = matita
-VERSION = 0.1.0
+VERSION = @MATITA_VERSION@
 
 NULL =
 DISTDIR = $(BASENAME)-$(VERSION)
diff --git a/helm/Makefile.defs.in b/helm/Makefile.defs.in
new file mode 100644
index 000000000..28adb2a19
--- /dev/null
+++ b/helm/Makefile.defs.in
@@ -0,0 +1,7 @@
+OCAMLFIND = OCAMLPATH=@OCAMLPATH@ @OCAMLFIND@
+CAMLP4O = @CAMLP4O@
+LABLGLADECC = @LABLGLADECC@
+HAVE_OCAMLOPT = @HAVE_OCAMLOPT@
+
+MATITA_REQUIRES = @FINDLIB_REQUIRES@
+MATITA_CREQUIRES = @FINDLIB_CREQUIRES@
diff --git a/helm/configure.ac b/helm/configure.ac
index c07a962ae..176763719 100644
--- a/helm/configure.ac
+++ b/helm/configure.ac
@@ -1,9 +1,9 @@
-AC_INIT(matitaTypes.ml)
+AC_INIT(matita/matitaTypes.ml)
 
 # Distribution settings (i.e. settings to be manipulated before a release)
 DEBUG_DEFAULT="true"
-RT_BASE_DIR_DEFAULT="`pwd`"
-MATITA_VERSION="0.0.1"
+RT_BASE_DIR_DEFAULT="`pwd`/matita"
+MATITA_VERSION="0.1.0"
 # End of distribution settings
 
 AC_CHECK_PROG(HAVE_OCAMLC, ocamlc, yes, no)
@@ -32,6 +32,53 @@ if test $HAVE_CAMLP4O = "yes"; then
 else
   AC_MSG_ERROR(could not find camlp4o)
 fi
+
+# look for METAS dir
+
+OCAMLPATH=""
+LIBSPATH=""
+if test -d libs ; then
+  OCAMLPATH=`pwd`/libs/METAS
+  LIBSPATH=`pwd`/libs
+fi
+if test -d ocaml ; then
+  OCAMLPATH=`pwd`/ocaml/METAS
+  LIBSPATH=`pwd`/ocaml
+fi
+if test -z $OCAMLPATH; then
+  AC_MSG_ERROR(could not find METAS directory)
+fi
+
+# creating META.*
+
+echo -n "creating METAs ... "
+for f in $OCAMLPATH/meta.*.src; do
+  basename=`basename $f`
+  metaname=`echo $basename | sed 's/meta\.\(.*\)\.src/\1/'`
+  dirname=`echo $metaname | sed 's/^helm-//'`
+  metafile="$OCAMLPATH/META.$metaname"
+  cp $f $metafile
+  echo "directory=\"$LIBSPATH/$dirname\"" >> $metafile
+done
+echo "done"
+
+# (libs) findlib requisites
+
+FINDLIB_LIBSREQUIRES="\
+expat \
+gdome2 \
+http \
+lablgtk2 \
+lablgtkmathview \
+lablgtksourceview \
+mysql \
+netstring \
+ulex \
+zip \
+"
+
+# (Matita) findlib requisites
+
 FINDLIB_COMREQUIRES="\
 helm-cic_disambiguation \
 helm-grafite \
@@ -40,12 +87,6 @@ helm-grafite_parser \
 helm-hgdome \
 helm-tactics \
 "
-FINDLIB_CLEANREQUIRES="$FINDLIB_COMREQUIRES"
-FINDLIB_DEPREQUIRES="$FINDLIB_COMREQUIRES"
-FINDLIB_MAKEREQUIRES=" \
-helm-registry \
-helm-extlib \
-"
 FINDLIB_CREQUIRES=" \
 $FINDLIB_COMREQUIRES \
 "
@@ -56,10 +97,10 @@ lablgtkmathview \
 lablgtksourceview \
 helm-xmldiff \
 "
-for r in $FINDLIB_REQUIRES
+for r in $FINDLIB_LIBSREQUIRES $FINDLIB_REQUIRES
 do
   AC_MSG_CHECKING(for $r ocaml library)
-  if OCAMLPATH=../ocaml/METAS $OCAMLFIND query $r &> /dev/null; then
+  if OCAMLPATH=$OCAMLPATH $OCAMLFIND query $r &> /dev/null; then
     AC_MSG_RESULT(yes)
   else
     AC_MSG_ERROR(could not find $r ocaml library)
@@ -117,18 +158,16 @@ AC_SUBST(DEBUG)
 AC_SUBST(TRANSFORMER_MODULE)
 AC_SUBST(FINDLIB_REQUIRES)
 AC_SUBST(FINDLIB_CREQUIRES)
-AC_SUBST(FINDLIB_DEPREQUIRES)
-AC_SUBST(FINDLIB_CLEANREQUIRES)
-AC_SUBST(FINDLIB_MAKEREQUIRES)
 AC_SUBST(HAVE_OCAMLOPT)
 AC_SUBST(LABLGLADECC)
 AC_SUBST(OCAMLFIND)
+AC_SUBST(OCAMLPATH)
 AC_SUBST(RT_BASE_DIR)
 AC_SUBST(MATITA_VERSION)
 
 AC_OUTPUT([
-  matita.conf.xml.sample
-  buildTimeConf.ml
-  Makefile
-  gtkmathview.matita.conf.xml
+  matita/matita.conf.xml.sample
+  matita/buildTimeConf.ml
+  matita/gtkmathview.matita.conf.xml
+  Makefile.defs
 ])
diff --git a/helm/matita/Makefile b/helm/matita/Makefile
new file mode 100644
index 000000000..3f65ab538
--- /dev/null
+++ b/helm/matita/Makefile
@@ -0,0 +1,307 @@
+export SHELL=/bin/bash
+
+include ../Makefile.defs
+
+NULL =
+H=@
+
+OCAML_FLAGS = -pp $(CAMLP4O)
+PKGS = -package "$(MATITA_REQUIRES)"
+CPKGS = -package "$(MATITA_CREQUIRES)"
+OCAML_THREADS_FLAGS = -thread
+OCAML_DEBUG_FLAGS = -g
+OCAMLC_FLAGS = $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS)
+OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLC_FLAGS) $(OCAML_DEBUG_FLAGS)
+OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS)
+OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS)
+
+MATITA_FLAGS = -noprofile
+NODB=false
+ifeq ($(NODB),true)
+	MATITA_FLAGS += -nodb
+endif
+
+# objects for matita (GTK GUI)
+CMOS =				\
+	buildTimeConf.cmo	\
+	matitaTypes.cmo		\
+	matitaMisc.cmo		\
+	matitamakeLib.cmo	\
+	matitaInit.cmo		\
+	matitaExcPp.cmo 	\
+	matitaEngine.cmo	\
+	matitacLib.cmo		\
+	matitaScript.cmo	\
+	matitaGeneratedGui.cmo	\
+	matitaGtkMisc.cmo	\
+	applyTransformation.cmo	\
+	matitaMathView.cmo 	\
+	matitaGui.cmo		\
+	$(NULL)
+# objects for matitac (batch compiler)
+CCMOS =				\
+	buildTimeConf.cmo	\
+	matitaTypes.cmo		\
+	matitaMisc.cmo		\
+	matitamakeLib.cmo	\
+	matitaInit.cmo		\
+	matitaExcPp.cmo 	\
+	matitaEngine.cmo	\
+	matitacLib.cmo		\
+	$(NULL)
+MAINCMOS =			\
+	matitadep.cmo		\
+	matitaclean.cmo		\
+	matitamake.cmo		\
+	$(NULL)
+PROGRAMS_BYTE = matita matitac cicbrowser matitadep matitaclean matitamake dump_moo
+PROGRAMS = $(PROGRAMS_BYTE) matitatop
+PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE))
+
+.PHONY: all
+all: matita.conf.xml $(PROGRAMS) coq.moo
+
+matita.conf.xml: matita.conf.xml.sample
+	@if diff matita.conf.xml.sample matita.conf.xml 1>/dev/null 2>/dev/null; then\
+		touch matita.conf.xml;\
+	else\
+		echo;\
+		echo "matita.conf.xml.sample is newer than matita.conf.xml";\
+		echo;\
+		echo "PLEASE update your configuration file!";\
+		echo "(copying matita.conf.xml.sample should work)";\
+		echo;\
+		false;\
+	fi
+
+matita.conf.xml.sample: matita.conf.xml.sample.in
+	autoconf
+	./configure
+	@echo 
+	@echo "WARNING: The configuration sample file has changed!"
+	@echo 
+
+coq.moo: library/legacy/coq.ma matitac
+	./matitac $(MATITA_FLAGS) $<
+coq.moo.opt: library/legacy/coq.ma matitac.opt
+	./matitac.opt $(MATITA_FLAGS) $<
+
+ifeq ($(HAVE_OCAMLOPT),yes)
+
+CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
+CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS))
+MAINCMXS = $(patsubst %.cmo,%.cmx,$(MAINCMOS))
+LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_REQUIRES))
+LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_REQUIRES))
+CLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MATITA_CREQUIRES))
+CLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MATITA_CREQUIRES))
+.PHONY: opt
+opt: $(PROGRAMS_OPT) coq.moo.opt
+.PHONY: upx
+upx: $(PROGRAMS_UPX) coq.moo.opt
+
+else
+
+opt:
+	@echo "Native code compilation is disabled"
+
+endif
+
+matita: matita.ml $(LIB_DEPS) $(CMOS)
+	@echo "OCAMLC $<"
+	$(H)$(OCAMLC) $(PKGS) -linkpkg -o $@ $(CMOS) matita.ml
+matita.opt: matita.ml $(LIBX_DEPS) $(CMXS)
+	@echo "OCAMLOPT $<"
+	$(H)$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml
+
+dump_moo: dump_moo.ml buildTimeConf.cmo
+	@echo "OCAMLC $<"
+	$(H)$(OCAMLC) $(PKGS) -linkpkg -o $@ buildTimeConf.cmo $<
+dump_moo.opt: dump_moo.ml buildTimeConf.cmx
+	@echo "OCAMLOPT $<"
+	$(H)$(OCAMLOPT) $(PKGS) -linkpkg -o $@ buildTimeConf.cmx $<
+
+matitac: matitac.ml $(CLIB_DEPS) $(CCMOS) $(MAINCMOS)
+	@echo "OCAMLC $<"
+	$(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) $(MAINCMOS) matitac.ml
+matitac.opt: matitac.ml $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS)
+	@echo "OCAMLOPT $<"
+	$(H)$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml
+
+matitatop: matitatop.ml $(CLIB_DEPS) $(CCMOS)
+	@echo "OCAMLC $<"
+	$(H)$(OCAMLC) $(CPKGS) -linkpkg -o $@ toplevellib.cma $(CCMOS) $<
+
+matitadep: matitac
+	@test -f $@ || ln -s $< $@
+matitadep.opt: matitac.opt
+	@test -f $@ || ln -s $< $@
+
+matitaclean: matitac
+	@test -f $@ || ln -s $< $@
+matitaclean.opt: matitac.opt
+	@test -f $@ || ln -s $< $@
+
+matitamake: matitac
+	@test -f $@ || ln -s $< $@
+matitamake.opt: matitac.opt
+	@test -f $@ || ln -s $< $@
+	
+cicbrowser: matita
+	@test -f $@ || ln -s $< $@
+cicbrowser.opt: matita.opt
+	@test -f $@ || ln -s $< $@
+
+matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade
+	$(LABLGLADECC) -embed $< > matitaGeneratedGui.ml
+	$(OCAMLC) $(PKGS) -i matitaGeneratedGui.ml > matitaGeneratedGui.mli
+
+.PHONY: clean
+clean:
+	rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \
+		$(PROGRAMS) \
+		$(PROGRAMS_OPT) \
+		$(PROGRAMS_STATIC) \
+		$(PROGRAMS_UPX) \
+		$(NULL)
+
+TEST_DIRS = 				\
+	library 			\
+	tests 				\
+	tests/bad_tests 		\
+	contribs/LAMBDA-TYPES 		\
+	contribs/PREDICATIVE-TOPOLOGY 	\
+	$(NULL)
+
+.PHONY: tests tests.opt cleantests cleantests.opt
+tests: $(foreach d,$(TEST_DIRS),$(d)-test)
+tests.opt: $(foreach d,$(TEST_DIRS),$(d)-test-opt)
+cleantests: $(foreach d,$(TEST_DIRS),$(d)-cleantests)
+cleantests.opt: $(foreach d,$(TEST_DIRS),$(d)-cleantests-opt)
+
+%-test: matitac matitadep matitaclean coq.moo
+	-cd $* && make -k clean all
+%-test-opt: matitac.opt matitadep.opt matitaclean.opt coq.moo.opt
+	-cd $* && make -k clean.opt opt
+%-cleantests: matitaclean
+	-cd $* && make clean
+%-cleantests-opt: matitaclean.opt
+	-cd $* && make clean.opt
+
+# {{{ Distribution stuff
+
+STATIC_LINK = dist/static_link/static_link
+# for matita
+STATIC_LIBS =	\
+	t1 t1x	\
+	gtkmathview_gmetadom mathview mathview_backend_gtk mathview_frontend_gmetadom \
+	gtksourceview-1.0 \
+	gdome gmetadom_gdome_cpp_smart \
+	stdc++ \
+	mysqlclient \
+	expat \
+	$(NULL)
+STATIC_EXTRA_LIBS = -cclib -lt1x -cclib -lstdc++
+# for matitac & co
+STATIC_CLIBS = \
+	gdome \
+	mysqlclient \
+	$(NULL)
+STATIC_EXTRA_CLIBS =
+PROGRAMS_STATIC = $(patsubst %,%.static,$(PROGRAMS_OPT))
+PROGRAMS_UPX = $(patsubst %,%.upx,$(PROGRAMS_STATIC))
+
+ifeq ($(HAVE_OCAMLOPT),yes)
+static: $(STATIC_LINK) $(PROGRAMS_STATIC) coq.moo.opt
+else
+upx:
+	@echo "Native code compilation is disabled"
+static:
+	@echo "Native code compilation is disabled"
+endif
+
+$(STATIC_LINK):
+	$(MAKE) -C dist/ $(STATIC_LINK)
+
+matita.opt.static: $(STATIC_LINK) $(LIBX_DEPS) $(CMXS) matita.ml
+	$(STATIC_LINK) $(STATIC_LIBS) -- \
+		$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml \
+		$(STATIC_EXTRA_LIBS)
+	strip $@
+dump_moo.opt.static: $(STATIC_LINK) buildTimeConf.cmx dump_moo.ml
+	$(STATIC_LINK) $(STATIC_CLIBS) -- \
+		$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $^ \
+		$(STATIC_EXTRA_CLIBS)
+	strip $@
+matitac.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml
+	$(STATIC_LINK) $(STATIC_CLIBS) -- \
+		$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \
+		$(STATIC_EXTRA_CLIBS)
+	strip $@
+matitadep.opt.static: matitac.opt.static
+	@test -f $@ || ln -s $< $@
+matitaclean.opt.static: matitac.opt.static
+	@test -f $@ || ln -s $< $@
+matitamake.opt.static: matitac.opt.static
+	@test -f $@ || ln -s $< $@
+cicbrowser.opt.static: matita.opt.static
+	@test -f $@ || ln -s $< $@
+cicbrowser.opt.static.upx: matita.opt.static.upx
+	@test -f $@ || ln -s $< $@
+
+.PHONY: distclean
+distclean: clean
+	$(MAKE) -C dist/ clean
+	rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli
+	rm -f config.log config.status Makefile buildTimeConf.ml
+	rm -f matita.glade.bak matita.gladep.bak
+	rm -rf autom4te.cache/
+	rm -f configure matita.conf.xml.sample
+
+%.upx: %
+	cp $< $@
+	strip $@
+	upx $@
+
+# }}} End of distribution stuff
+
+tags: TAGS
+.PHONY: TAGS
+TAGS:
+	cd ..; otags -vi -r ocaml/ matita/
+
+#.depend: matitaGeneratedGui.ml matitaGeneratedGui.mli *.ml *.mli
+
+.PHONY: depend
+depend:
+	$(OCAMLDEP) *.ml *.mli > .depend
+
+include .depend
+
+%.cmi: %.mli
+	@echo "OCAMLC $<"
+	$(H)$(OCAMLC) $(PKGS) -c $<
+%.cmo %.cmi: %.ml
+	@echo "OCAMLC $<"
+	$(H)$(OCAMLC) $(PKGS) -c $<
+%.cmx: %.ml
+	@echo "OCAMLOPT $<"
+	$(H)$(OCAMLOPT) $(PKGS) -c $<
+%.annot: %.ml
+	@echo "OCAMLC -dtypes $<"
+	$(H)$(OCAMLC) -dtypes $(PKGS) -c $<
+
+$(CMOS): $(LIB_DEPS)
+$(CMOS:%.cmo=%.cmx): $(LIBX_DEPS)
+
+ifeq ($(MAKECMDGOALS),all)
+   $(CMOS:%.cmo=%.cmi): $(LIB_DEPS)
+endif
+ifeq ($(MAKECMDGOALS),)
+   $(CMOS:%.cmo=%.cmi): $(LIB_DEPS)
+endif
+ifeq ($(MAKECMDGOALS),opt)
+   $(CMOS:%.cmo=%.cmi): $(LIBX_DEPS)
+endif
+
+# vim: set foldmethod=marker:
diff --git a/helm/matita/Makefile.in b/helm/matita/Makefile.in
deleted file mode 100644
index af543d640..000000000
--- a/helm/matita/Makefile.in
+++ /dev/null
@@ -1,350 +0,0 @@
-export SHELL=/bin/bash
-
-NULL =
-
-MAKEFLAGS+=--no-print-directory
-OCAMLPATH = ../ocaml/METAS/
-OCAMLFIND = OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH @OCAMLFIND@
-CAMLP4O = @CAMLP4O@
-LABLGLADECC = @LABLGLADECC@
-REQUIRES = @FINDLIB_REQUIRES@
-CREQUIRES = @FINDLIB_CREQUIRES@
-DEPREQUIRES = @FINDLIB_DEPREQUIRES@
-CLEANREQUIRES = @FINDLIB_CLEANREQUIRES@
-MAKEREQUIRES = @FINDLIB_MAKEREQUIRES@
-HAVE_OCAMLOPT = @HAVE_OCAMLOPT@
-
-OCAML_FLAGS = -pp $(CAMLP4O)
-PKGS = -package "$(REQUIRES)"
-CPKGS = -package "$(CREQUIRES)"
-DEPPKGS = -package "$(DEPREQUIRES)"
-CLEANPKGS = -package "$(CLEANREQUIRES)"
-MAKEPKGS = -package "$(MAKEREQUIRES)"
-OCAML_THREADS_FLAGS = -thread
-OCAML_DEBUG_FLAGS = -g
-OCAMLC_FLAGS = $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS)
-OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLC_FLAGS) $(OCAML_DEBUG_FLAGS)
-OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS)
-OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS)
-
-MATITA_FLAGS = -noprofile
-NODB=false
-ifeq ($(NODB),true)
-	MATITA_FLAGS += -nodb
-endif
-
-# objects for matita (GTK GUI)
-CMOS =				\
-	buildTimeConf.cmo	\
-	matitaTypes.cmo		\
-	matitaMisc.cmo		\
-	matitamakeLib.cmo	\
-	matitaInit.cmo		\
-	matitaExcPp.cmo 	\
-	matitaEngine.cmo	\
-	matitacLib.cmo		\
-	matitaScript.cmo	\
-	matitaGeneratedGui.cmo	\
-	matitaGtkMisc.cmo	\
-	applyTransformation.cmo	\
-	matitaMathView.cmo 	\
-	matitaGui.cmo		\
-	$(NULL)
-# objects for matitac (batch compiler)
-CCMOS =				\
-	buildTimeConf.cmo	\
-	matitaTypes.cmo		\
-	matitaMisc.cmo		\
-	matitamakeLib.cmo	\
-	matitaInit.cmo		\
-	matitaExcPp.cmo 	\
-	matitaEngine.cmo	\
-	matitacLib.cmo		\
-	$(NULL)
-MAINCMOS =			\
-	matitadep.cmo		\
-	matitaclean.cmo		\
-	matitamake.cmo		\
-	$(NULL)
-DEPCMOS = $(CCMOS)
-CLEANCMOS = $(CCMOS)
-MAKECMOS = \
-	buildTimeConf.cmo	\
-	matitamakeLib.cmo	\
-	$(NULL)
-PROGRAMS_BYTE = matita matitac cicbrowser matitadep matitaclean matitamake dump_moo
-PROGRAMS = $(PROGRAMS_BYTE) matitatop
-PROGRAMS_OPT = $(patsubst %,%.opt,$(PROGRAMS_BYTE))
-
-.PHONY: all
-all: matita.conf.xml $(PROGRAMS) coq.moo
-
-matita.conf.xml: matita.conf.xml.sample
-	@if diff matita.conf.xml.sample matita.conf.xml 1>/dev/null 2>/dev/null; then\
-		touch matita.conf.xml;\
-	else\
-		echo;\
-		echo "matita.conf.xml.sample is newer than matita.conf.xml";\
-		echo;\
-		echo "PLEASE update your configuration file!";\
-		echo "(copying matita.conf.xml.sample should work)";\
-		echo;\
-		false;\
-	fi
-
-matita.conf.xml.sample: matita.conf.xml.sample.in
-	autoconf
-	./configure
-	@echo 
-	@echo "WARNING: The configuration sample file has changed!"
-	@echo 
-
-coq.moo: library/legacy/coq.ma matitac
-	./matitac $(MATITA_FLAGS) $<
-coq.moo.opt: library/legacy/coq.ma matitac.opt
-	./matitac.opt $(MATITA_FLAGS) $<
-
-ifeq ($(HAVE_OCAMLOPT),yes)
-
-CMXS = $(patsubst %.cmo,%.cmx,$(CMOS))
-CCMXS = $(patsubst %.cmo,%.cmx,$(CCMOS))
-MAINCMXS = $(patsubst %.cmo,%.cmx,$(MAINCMOS))
-DEPCMXS = $(patsubst %.cmo,%.cmx,$(DEPCMOS))
-CLEANCMXS = $(patsubst %.cmo,%.cmx,$(CLEANCMOS))
-MAKECMXS = $(patsubst %.cmo,%.cmx,$(MAKECMOS))
-LIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(REQUIRES))
-LIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(REQUIRES))
-CLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(CREQUIRES))
-CLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(CREQUIRES))
-DEPLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(DEPREQUIRES))
-DEPLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(DEPREQUIRES))
-CLEANLIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(CLEANREQUIRES))
-CLEANLIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(CLEANREQUIRES))
-MAKELIB_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "byte" -format "%d/%a" $(MAKEREQUIRES))
-MAKELIBX_DEPS := $(shell $(OCAMLFIND) query -recursive -predicates "native" -format "%d/%a" $(MAKEREQUIRES))
-.PHONY: opt
-opt: $(PROGRAMS_OPT) coq.moo.opt
-.PHONY: upx
-upx: $(PROGRAMS_UPX) coq.moo.opt
-
-else
-
-opt:
-	@echo "Native code compilation is disabled"
-
-endif
-
-matita: $(LIB_DEPS) $(CMOS) matita.ml
-	$(OCAMLC) $(PKGS) -linkpkg -o $@ $(CMOS) matita.ml
-matita.opt: $(LIBX_DEPS) $(CMXS) matita.ml
-	$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml
-
-dump_moo: buildTimeConf.cmo dump_moo.ml
-	$(OCAMLC) $(PKGS) -linkpkg -o $@ $^
-dump_moo.opt: buildTimeConf.cmx dump_moo.ml
-	$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $^
-
-matitac: $(CLIB_DEPS) $(CCMOS) $(MAINCMOS) matitac.ml
-	$(OCAMLC) $(CPKGS) -linkpkg -o $@ $(CCMOS) $(MAINCMOS) matitac.ml
-matitac.opt: $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml
-	$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml
-
-matitatop: matitatop.ml $(CLIB_DEPS) $(CCMOS)
-	$(OCAMLC) $(CPKGS) -linkpkg -o $@ toplevellib.cma $(CCMOS) $<
-
-#  matitadep: matitadep.ml $(DEPLIB_DEPS) $(DEPCMOS)
-#          $(OCAMLC) $(DEPPKGS) -linkpkg -o $@ $(DEPCMOS) $<
-#  matitadep.opt: matitadep.ml $(DEPLIB_DEPS) $(DEPCMXS)
-#          $(OCAMLOPT) $(DEPPKGS) -linkpkg -o $@ $(DEPCMXS) $<
-matitadep: matitac
-	@test -f $@ || ln -s $< $@
-matitadep.opt: matitac.opt
-	@test -f $@ || ln -s $< $@
-
-#  matitaclean: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMOS)
-#          $(OCAMLC) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMOS) $<
-#  matitaclean.opt: matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMXS)
-#          $(OCAMLOPT) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMXS) $<
-matitaclean: matitac
-	@test -f $@ || ln -s $< $@
-matitaclean.opt: matitac.opt
-	@test -f $@ || ln -s $< $@
-
-#  matitamake: matitamake.ml $(MAKECMOS)
-#          $(OCAMLC) $(MAKEPKGS) -linkpkg -o $@ $(MAKECMOS) $<
-#  matitamake.opt: matitamake.ml $(MAKECMXS)
-#          $(OCAMLOPT) $(MAKEPKGS) -linkpkg -o $@ $(MAKECMXS) $<
-matitamake: matitac
-	@test -f $@ || ln -s $< $@
-matitamake.opt: matitac.opt
-	@test -f $@ || ln -s $< $@
-	
-cicbrowser: matita
-	@test -f $@ || ln -s $< $@
-cicbrowser.opt: matita.opt
-	@test -f $@ || ln -s $< $@
-
-matitaGeneratedGui.ml matitaGeneratedGui.mli: matita.glade
-	$(LABLGLADECC) -embed $< > matitaGeneratedGui.ml
-	$(OCAMLC) $(PKGS) -i matitaGeneratedGui.ml > matitaGeneratedGui.mli
-
-.PHONY: clean
-clean:
-	rm -rf *.cma *.cmo *.cmi *.cmx *.cmxa *.a *.o \
-		$(PROGRAMS) \
-		$(PROGRAMS_OPT) \
-		$(PROGRAMS_STATIC) \
-		$(PROGRAMS_UPX) \
-		$(NULL)
-
-TEST_DIRS = 				\
-	library 			\
-	tests 				\
-	tests/bad_tests 		\
-	contribs/LAMBDA-TYPES 		\
-	contribs/PREDICATIVE-TOPOLOGY 	\
-	$(NULL)
-
-.PHONY: tests tests.opt cleantests cleantests.opt
-tests: $(foreach d,$(TEST_DIRS),$(d)-test)
-tests.opt: $(foreach d,$(TEST_DIRS),$(d)-test-opt)
-cleantests: $(foreach d,$(TEST_DIRS),$(d)-cleantests)
-cleantests.opt: $(foreach d,$(TEST_DIRS),$(d)-cleantests-opt)
-
-%-test: matitac matitadep matitaclean coq.moo
-	-cd $* && make -k clean all
-%-test-opt: matitac.opt matitadep.opt matitaclean.opt coq.moo.opt
-	-cd $* && make -k clean.opt opt
-%-cleantests: matitaclean
-	-cd $* && make clean
-%-cleantests-opt: matitaclean.opt
-	-cd $* && make clean.opt
-
-# {{{ Distribution stuff
-
-STATIC_LINK = dist/static_link/static_link
-# for matita
-STATIC_LIBS =	\
-	t1 t1x	\
-	gtkmathview_gmetadom mathview mathview_backend_gtk mathview_frontend_gmetadom \
-	gtksourceview-1.0 \
-	gdome gmetadom_gdome_cpp_smart \
-	stdc++ \
-	mysqlclient \
-	expat \
-	$(NULL)
-STATIC_EXTRA_LIBS = -cclib -lt1x -cclib -lstdc++
-# for matitac & co
-STATIC_CLIBS = \
-	gdome \
-	mysqlclient \
-	$(NULL)
-STATIC_EXTRA_CLIBS =
-PROGRAMS_STATIC = $(patsubst %,%.static,$(PROGRAMS_OPT))
-PROGRAMS_UPX = $(patsubst %,%.upx,$(PROGRAMS_STATIC))
-
-ifeq ($(HAVE_OCAMLOPT),yes)
-static: $(STATIC_LINK) $(PROGRAMS_STATIC) coq.moo.opt
-else
-upx:
-	@echo "Native code compilation is disabled"
-static:
-	@echo "Native code compilation is disabled"
-endif
-
-$(STATIC_LINK):
-	$(MAKE) -C dist/ $(STATIC_LINK)
-
-matita.opt.static: $(STATIC_LINK) $(LIBX_DEPS) $(CMXS) matita.ml
-	$(STATIC_LINK) $(STATIC_LIBS) -- \
-		$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(CMXS) matita.ml \
-		$(STATIC_EXTRA_LIBS)
-	strip $@
-dump_moo.opt.static: $(STATIC_LINK) buildTimeConf.cmx dump_moo.ml
-	$(STATIC_LINK) $(STATIC_CLIBS) -- \
-		$(OCAMLOPT) $(PKGS) -linkpkg -o $@ $^ \
-		$(STATIC_EXTRA_CLIBS)
-	strip $@
-matitac.opt.static: $(STATIC_LINK) $(CLIBX_DEPS) $(CCMXS) $(MAINCMXS) matitac.ml
-	$(STATIC_LINK) $(STATIC_CLIBS) -- \
-		$(OCAMLOPT) $(CPKGS) -linkpkg -o $@ $(CCMXS) $(MAINCMXS) matitac.ml \
-		$(STATIC_EXTRA_CLIBS)
-	strip $@
-#  matitadep.opt.static: $(STATIC_LINK) matitadep.ml $(DEPLIB_DEPS) $(DEPCMXS)
-#          $(STATIC_LINK) $(STATIC_CLIBS) -- \
-#                  $(OCAMLOPT) $(DEPPKGS) -linkpkg -o $@ $(DEPCMXS) $< \
-#                  $(STATIC_EXTRA_CLIBS)
-#          strip $@
-matitadep.opt.static: matitac.opt.static
-	@test -f $@ || ln -s $< $@
-#  matitaclean.opt.static: $(STATIC_LINK) matitaclean.ml $(CLEANLIB_DEPS) $(CLEANCMXS)
-#          $(STATIC_LINK) $(STATIC_CLIBS) -- \
-#                  $(OCAMLOPT) $(CLEANPKGS) -linkpkg -o $@ $(CLEANCMXS) $< \
-#                  $(STATIC_EXTRA_CLIBS)
-#          strip $@
-matitaclean.opt.static: matitac.opt.static
-	@test -f $@ || ln -s $< $@
-#  matitamake.opt.static: $(STATIC_LINK) matitamake.ml $(MAKECMXS)
-#          $(STATIC_LINK) $(STATIC_CLIBS) -- \
-#                  $(OCAMLOPT) $(PKGS) -linkpkg -o $@ $(MAKECMXS) $< \
-#                  $(STATIC_EXTRA_CLIBS)
-#          strip $@
-matitamake.opt.static: matitac.opt.static
-	@test -f $@ || ln -s $< $@
-cicbrowser.opt.static: matita.opt.static
-	@test -f $@ || ln -s $< $@
-cicbrowser.opt.static.upx: matita.opt.static.upx
-	@test -f $@ || ln -s $< $@
-
-.PHONY: distclean
-distclean: clean
-	$(MAKE) -C dist/ clean
-	rm -f matitaGeneratedGui.ml matitaGeneratedGui.mli
-	rm -f config.log config.status Makefile buildTimeConf.ml
-	rm -f matita.glade.bak matita.gladep.bak
-	rm -rf autom4te.cache/
-	rm -f configure matita.conf.xml.sample
-
-%.upx: %
-	cp $< $@
-	strip $@
-	upx $@
-
-# }}} End of distribution stuff
-
-tags: TAGS
-.PHONY: TAGS
-TAGS:
-	cd ..; otags -vi -r ocaml/ matita/
-
-#.depend: matitaGeneratedGui.ml matitaGeneratedGui.mli *.ml *.mli
-
-.PHONY: depend
-depend:
-	$(OCAMLDEP) *.ml *.mli > .depend
-
-include .depend
-
-%.cmi: %.mli
-	$(OCAMLC) $(PKGS) -c $<
-%.cmo %.cmi: %.ml
-	$(OCAMLC) $(PKGS) -c $<
-%.cmx: %.ml
-	$(OCAMLOPT) $(PKGS) -c $<
-%.annot: %.ml
-	$(OCAMLC) -dtypes $(PKGS) -c $<
-
-$(CMOS): $(LIB_DEPS)
-$(CMOS:%.cmo=%.cmx): $(LIBX_DEPS)
-
-ifeq ($(MAKECMDGOALS),all)
-   $(CMOS:%.cmo=%.cmi): $(LIB_DEPS)
-endif
-ifeq ($(MAKECMDGOALS),)
-   $(CMOS:%.cmo=%.cmi): $(LIB_DEPS)
-endif
-ifeq ($(MAKECMDGOALS),opt)
-   $(CMOS:%.cmo=%.cmi): $(LIBX_DEPS)
-endif
-
-# vim: set foldmethod=marker:
diff --git a/helm/matita/configure.ac b/helm/matita/configure.ac
deleted file mode 100644
index c07a962ae..000000000
--- a/helm/matita/configure.ac
+++ /dev/null
@@ -1,134 +0,0 @@
-AC_INIT(matitaTypes.ml)
-
-# Distribution settings (i.e. settings to be manipulated before a release)
-DEBUG_DEFAULT="true"
-RT_BASE_DIR_DEFAULT="`pwd`"
-MATITA_VERSION="0.0.1"
-# End of distribution settings
-
-AC_CHECK_PROG(HAVE_OCAMLC, ocamlc, yes, no)
-if test $HAVE_OCAMLC = "no"; then
-  AC_MSG_ERROR(could not find ocamlc)
-fi
-AC_CHECK_PROG(HAVE_OCAMLOPT, ocamlopt, yes, no)
-if test $HAVE_OCAMLOPT = "no"; then
-  AC_MSG_WARN(could not find ocamlopt: native code compilation disabled)
-fi
-AC_CHECK_PROG(HAVE_OCAMLFIND, ocamlfind, yes, no)
-if test $HAVE_OCAMLFIND = "yes"; then
-  OCAMLFIND="ocamlfind"
-else
-  AC_MSG_ERROR(could not find ocamlfind)
-fi
-AC_CHECK_PROG(HAVE_LABLGLADECC, lablgladecc2, yes, no)
-if test $HAVE_LABLGLADECC = "yes"; then
-  LABLGLADECC="lablgladecc2"
-else
-  AC_MSG_ERROR(could not find lablgladecc2)
-fi
-AC_CHECK_PROG(HAVE_CAMLP4O, camlp4o, yes, no)
-if test $HAVE_CAMLP4O = "yes"; then
-  CAMLP4O="camlp4o"
-else
-  AC_MSG_ERROR(could not find camlp4o)
-fi
-FINDLIB_COMREQUIRES="\
-helm-cic_disambiguation \
-helm-grafite \
-helm-grafite_engine \
-helm-grafite_parser \
-helm-hgdome \
-helm-tactics \
-"
-FINDLIB_CLEANREQUIRES="$FINDLIB_COMREQUIRES"
-FINDLIB_DEPREQUIRES="$FINDLIB_COMREQUIRES"
-FINDLIB_MAKEREQUIRES=" \
-helm-registry \
-helm-extlib \
-"
-FINDLIB_CREQUIRES=" \
-$FINDLIB_COMREQUIRES \
-"
-FINDLIB_REQUIRES="\
-$FINDLIB_CREQUIRES \
-lablgtk2.glade \
-lablgtkmathview \
-lablgtksourceview \
-helm-xmldiff \
-"
-for r in $FINDLIB_REQUIRES
-do
-  AC_MSG_CHECKING(for $r ocaml library)
-  if OCAMLPATH=../ocaml/METAS $OCAMLFIND query $r &> /dev/null; then
-    AC_MSG_RESULT(yes)
-  else
-    AC_MSG_ERROR(could not find $r ocaml library)
-  fi
-done
-
-OCAMLFIND_COMMANDS=""
-# AC_CHECK_PROG(HAVE_OCAMLC_OPT, ocamlc.opt, yes, no)
-# if test $HAVE_OCAMLC_OPT = "yes"; then
-#   if test "$OCAMLFIND_COMMANDS" = ""; then
-#     OCAMLFIND_COMMANDS="ocamlc=ocamlc.opt"
-#   else
-#     OCAMLFIND_COMMANDS="$OCAMLFIND_COMMANDS ocamlc=ocamlc.opt"
-#   fi
-# fi
-# AC_CHECK_PROG(HAVE_OCAMLOPT_OPT, ocamlopt.opt, yes, no)
-# if test $HAVE_OCAMLOPT_OPT = "yes"; then
-#   if test "$OCAMLFIND_COMMANDS" = ""; then
-#     OCAMLFIND_COMMANDS="ocamlopt=ocamlopt.opt"
-#   else
-#     OCAMLFIND_COMMANDS="$OCAMLFIND_COMMANDS ocamlopt=ocamlopt.opt"
-#   fi
-# fi
-if test "$OCAMLFIND_COMMANDS" != ""; then
-  OCAMLFIND="OCAMLFIND_COMMANDS='$OCAMLFIND_COMMANDS' $OCAMLFIND"
-fi
-
-AC_MSG_CHECKING(--enable-debug argument)
-AC_ARG_ENABLE(debug,
-  [  --enable-debug	Turn on debugging],
-  [GIVEN="yes";
-   case "${enableval}" in
-   yes) DEBUG=true ;;
-   no)  DEBUG=false ;;
-   *) AC_MSG_ERROR(bad value ${enableval} for --enable-debug) ;;
-  esac],
-  [GIVEN="no"; DEBUG="$DEBUG_DEFAULT"])
-MSG=$GIVEN
-if test "$DEBUG" = "true"; then
-  MSG="$MSG, debugging enabled."
-else
-  MSG="$MSG, debugging disabled."
-fi
-AC_MSG_RESULT($MSG)
-
-AC_MSG_CHECKING(--with-runtime-dir argument)
-AC_ARG_WITH(runtime-dir,
-  [ --with-runtime-dir	Runtime directory (current working directory if not given)],
-  [ RT_BASE_DIR="${withval}" ],
-  [ RT_BASE_DIR="$RT_BASE_DIR_DEFAULT" ])
-AC_MSG_RESULT($RT_BASE_DIR)
-
-AC_SUBST(CAMLP4O)
-AC_SUBST(DEBUG)
-AC_SUBST(TRANSFORMER_MODULE)
-AC_SUBST(FINDLIB_REQUIRES)
-AC_SUBST(FINDLIB_CREQUIRES)
-AC_SUBST(FINDLIB_DEPREQUIRES)
-AC_SUBST(FINDLIB_CLEANREQUIRES)
-AC_SUBST(FINDLIB_MAKEREQUIRES)
-AC_SUBST(HAVE_OCAMLOPT)
-AC_SUBST(LABLGLADECC)
-AC_SUBST(OCAMLFIND)
-AC_SUBST(RT_BASE_DIR)
-AC_SUBST(MATITA_VERSION)
-
-AC_OUTPUT([
-  matita.conf.xml.sample
-  buildTimeConf.ml
-  Makefile
-  gtkmathview.matita.conf.xml
-])
diff --git a/helm/ocaml/Makefile b/helm/ocaml/Makefile
new file mode 100644
index 000000000..0d1867293
--- /dev/null
+++ b/helm/ocaml/Makefile
@@ -0,0 +1,120 @@
+
+export SHELL=/bin/bash
+
+include ../Makefile.defs
+
+# Warning: the modules must be in compilation order
+NULL =
+MODULES =			\
+	extlib			\
+	xml			\
+	hgdome			\
+	registry		\
+ 	hmysql 			\
+	utf8_macros		\
+	thread			\
+	xmldiff			\
+	urimanager		\
+	logger			\
+	getter			\
+	cic			\
+	cic_proof_checking	\
+	cic_acic		\
+	acic_content		\
+	content_pres		\
+	grafite			\
+	metadata		\
+	library			\
+	cic_unification		\
+	whelp			\
+	tactics			\
+	cic_disambiguation	\
+	lexicon			\
+	grafite_engine          \
+	grafite_parser          \
+	tactics/paramodulation 	\
+	$(NULL)
+
+METAS = $(filter-out %/paramodulation,$(MODULES:%=METAS/META.helm-%))
+
+all: metas $(MODULES:%=%.all) 
+opt: metas $(MODULES:%=%.opt)
+world: all opt
+depend: $(MODULES:%=%.depend)
+install: $(MODULES:%=%.install)
+uninstall: $(MODULES:%=%.uninstall)
+clean: $(MODULES:%=%.clean) clean_metas
+
+.stats: $(MODULES:%=%.stats)
+	(for m in $(MODULES); do echo -n "$$m:"; cat $$m/.stats; done) \
+	 | sort -t : -k 2 -n -r > .stats
+
+EXTRA_DIST_CLEAN = \
+	libraries-clusters.ps 	\
+	libraries-clusters.pdf 	\
+	libraries-ext.ps 	\
+	libraries.ps 		\
+	.dep.dot 		\
+	.extdep.dot 		\
+	.clustersdep.dot 	\
+	$(NULL)
+
+distclean: clean clean_metas
+	rm -f $(METAS)
+	rm -f configure config.log config.cache config.status
+	rm -f Makefile Makefile.common $(EXTRA_DIST_CLEAN)
+
+.PHONY: all opt world metas depend install uninstall clean clean_metas distclean
+
+%.all:
+	$(MAKE) -C $* all 
+%.opt:
+	$(MAKE) -C $* opt
+%.clean:
+	$(MAKE) -C $* clean 
+%.depend:
+	$(MAKE) -C $* depend 
+%.stats:
+	@$(MAKE) -C $* .stats
+
+METAS/META.helm-%: METAS/meta.helm-%.src
+	cp $< $@ && echo "directory=\"$(shell pwd)/$*\"" >> $@
+
+.PHONY: .dep.dot
+.dep.dot:
+	echo "digraph G {" > $@
+	echo "   rankdir = TB ;" >> $@
+	for i in $(MODULES); do $(OCAMLFIND) query helm-$$i -recursive -p-format | grep helm | sed "s/^helm-/ \"$$i\" -> \"/g" | sed "s/$$/\";/g" >> $@ ; done
+	mv $@ $@.old ; ./simplify_deps/simplify_deps.opt < $@.old > $@ ; rm $@.old
+	echo "}" >> $@
+
+.PHONY: .alldep.dot
+.alldep.dot:
+	echo "digraph G {" > $@
+	echo "   rankdir = TB ;" >> $@
+	for i in $(MODULES); do $(OCAMLFIND) query helm-$$i -recursive -p-format | grep -v "pxp-" | sed "s/^pxp/pxp[-*]/g" | sed "s/^/ \"helm-$$i\" -> \"/g" | sed "s/$$/\";/g" >> $@ ; done
+	mv $@ $@.old ; ./simplify_deps/simplify_deps.opt < $@.old > $@ ; rm $@.old
+	for i in $(MODULES); do echo "\"helm-$$i\" [shape=box,style=filled,fillcolor=yellow];" >> $@ ; done
+	echo "}" >> $@
+
+.extdep.dot: .dep.dot
+	STATS/patch_deps.sh $< $@
+.clustersdep.dot: .dep.dot
+	USE_CLUSTERS=yes STATS/patch_deps.sh $< $@
+
+libraries.ps: .dep.dot
+	dot -Tps -o $@ $<
+libraries-ext.ps: .extdep.dot
+	dot -Tps -o $@ $<
+libraries-clusters.ps: .clustersdep.dot
+	dot -Tps -o $@ $<
+libraries-complete.ps: .alldep.dot
+	dot -Tps -o $@ $<
+
+ps: libraries.ps libraries-ext.ps libraries-clusters.ps
+
+tags: TAGS
+.PHONY: TAGS
+TAGS:
+	otags -vi -r .
+
diff --git a/helm/ocaml/Makefile.common b/helm/ocaml/Makefile.common
new file mode 100644
index 000000000..1a8b029f9
--- /dev/null
+++ b/helm/ocaml/Makefile.common
@@ -0,0 +1,133 @@
+H=@
+
+# This Makefile must be included by another one defining:
+#  $PACKAGE
+#  $PREDICATES
+#  $INTERFACE_FILES
+#  $IMPLEMENTATION_FILES
+#  $EXTRA_OBJECTS_TO_INSTALL
+#  $EXTRA_OBJECTS_TO_CLEAN
+# and put in a directory where there is a .depend file.
+
+# $OCAMLFIND must be set to a meaningful vaule, including OCAMLPATH=
+
+PREPROCOPTIONS = -pp camlp4o
+SYNTAXOPTIONS = -syntax camlp4o
+PREREQ =
+OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread
+OCAMLDEBUGOPTIONS = -g
+OCAMLARCHIVEOPTIONS =
+REQUIRES := $(shell $(OCAMLFIND) -query -format '%(requires)' helm-$(PACKAGE))
+OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS) $(PREPROCOPTIONS)
+OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) $(PREPROCOPTIONS)
+OCAMLDEP = $(OCAMLFIND) ocamldep -package "camlp4 $(CAMLP4REQUIRES)" $(SYNTAXOPTIONS) $(OCAMLDEPOPTIONS) 
+OCAMLLEX = ocamllex
+OCAMLYACC = ocamlyacc
+
+OCAMLC_P4 = $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS) $(SYNTAXOPTIONS)
+OCAMLOPT_P4 = $(OCAMLFIND) opt $(OCAMLOPTIONS) $(SYNTAXOPTIONS)
+
+LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES))
+LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES))
+LIBRARIES_DEPS := \
+	$(foreach X,$(filter-out /usr/lib/ocaml%,$(LIBRARIES)),\
+		$(wildcard \
+			$(shell dirname $(X))/*.mli \
+			$(shell dirname $(X))/*.ml \
+			$(shell dirname $(X))/paramodulation/*.ml \
+			$(shell dirname $(X))/paramodultation/*.mli))
+
+
+ARCHIVE = $(PACKAGE).cma
+ARCHIVE_OPT = $(PACKAGE).cmxa
+OBJECTS_TO_INSTALL = $(ARCHIVE) $(ARCHIVE_OPT) $(ARCHIVE_OPT:%.cmxa=%.a) \
+                     $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.cmi) \
+                     $(EXTRA_OBJECTS_TO_INSTALL)
+DEPEND_FILES = $(INTERFACE_FILES) $(IMPLEMENTATION_FILES)
+
+$(ARCHIVE): $(IMPLEMENTATION_FILES:%.ml=%.cmo) $(LIBRARIES)
+	$(H)if [ $(PACKAGE) != dummy ]; then \
+	echo "  OCAMLC -a $@";\
+	$(OCAMLC) $(OCAMLARCHIVEOPTIONS) -a -o $@ \
+		$(IMPLEMENTATION_FILES:%.ml=%.cmo); fi
+
+$(ARCHIVE_OPT): $(IMPLEMENTATION_FILES:%.ml=%.cmx) $(LIBRARIES_OPT)
+	$(H)if [ $(PACKAGE) != dummy ]; then \
+	echo "  OCAMLOPT -a $@";\
+	$(OCAMLOPT) $(OCAMLARCHIVEOPTIONS) -a -o $@ \
+		$(IMPLEMENTATION_FILES:%.ml=%.cmx); fi
+
+prereq: $(PREREQ)
+all: prereq $(IMPLEMENTATION_FILES:%.ml=%.cmo) $(ARCHIVE)
+	@echo -n 
+opt: prereq $(IMPLEMENTATION_FILES:%.ml=%.cmx) $(ARCHIVE_OPT)
+	@echo -n 
+world: all opt
+test: test.ml $(ARCHIVE)
+	$(OCAMLC) $(ARCHIVE) -linkpkg -o $@ $<
+test.opt: test.ml $(ARCHIVE_OPT)
+	$(OCAMLOPT) $(ARCHIVE_OPT) -linkpkg -o $@ $<
+
+depend: $(DEPEND_FILES)
+	$(OCAMLDEP) $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend
+
+$(PACKAGE).ps: .dep.dot
+	dot -Tps -o $@ $<
+
+.dep.dot: .depend
+	ocamldot < .depend > $@
+
+%.cmi: %.mli
+	@echo "  OCAMLC $<"
+	$(H)$(OCAMLC) -c $<
+%.cmo %.cmi: %.ml
+	@echo "  OCAMLC $<"
+	$(H)$(OCAMLC) -c $<
+%.cmx: %.ml
+	@echo "  OCAMLOPT $<"
+	$(H)$(OCAMLOPT) -c $<
+%.annot: %.ml
+	$(OCAMLC) -dtypes $(PKGS) -c $<
+%.ml %.mli: %.mly
+	$(OCAMLYACC) $<
+%.ml: %.mll
+	$(OCAMLLEX) $<
+
+ifneq ($(MAKECMDGOALS), clean)
+$(IMPLEMENTATION_FILES:%.ml=%.cmo): $(LIBRARIES)
+$(IMPLEMENTATION_FILES:%.ml=%.cmi): $(LIBRARIES_DEPS)
+$(IMPLEMENTATION_FILES:%.ml=%.cmx): $(LIBRARIES_OPT)
+endif
+
+clean:
+	rm -f *.cm[ioax] *.cmxa *.o *.a *.annot $(EXTRA_OBJECTS_TO_CLEAN)
+	if [ -f test ]; then rm -f test; else true; fi
+	if [ -f test.opt ]; then rm -f test.opt; else true; fi
+
+backup:
+	cd ..; tar cvzf $(PACKAGE)_$(shell date +%s).tar.gz $(PACKAGE)
+
+ocamlinit:
+	echo "#use \"topfind\";;" > .ocamlinit
+	echo "#thread;;" >> .ocamlinit
+	for p in $(REQUIRES); do echo "#require \"$$p\";;" >> .ocamlinit; done
+	echo "#load \"$(PACKAGE).cma\";;" >> .ocamlinit
+
+# $(STATS_EXCLUDE) may be defined in libraries' Makefile to exclude some file
+# from statistics collection
+STATS_FILES = \
+	$(shell find . -maxdepth 1 -type f -name \*.ml $(foreach f,$(STATS_EXCLUDE),-not -name $(f))) \
+	$(shell find . -maxdepth 1 -type f -name \*.mli $(foreach f,$(STATS_EXCLUDE),-not -name $(f)))
+.stats: $(STATS_FILES)
+	rm -f .stats
+	echo -n "LOC:" >> .stats
+	wc -l $(STATS_FILES) | tail -1 | awk '{ print $$1 }' >> .stats
+
+.PHONY: all opt world backup depend install uninstall clean ocamlinit
+
+ifneq ($(MAKECMDGOALS), depend)
+   include .depend   
+endif
+
+NULL =
+
diff --git a/helm/ocaml/Makefile.common.in b/helm/ocaml/Makefile.common.in
deleted file mode 100644
index 800bcf7c7..000000000
--- a/helm/ocaml/Makefile.common.in
+++ /dev/null
@@ -1,141 +0,0 @@
-H=@
-
-# This Makefile must be included by another one defining:
-#  $PACKAGE
-#  $PREDICATES
-#  $INTERFACE_FILES
-#  $IMPLEMENTATION_FILES
-#  $EXTRA_OBJECTS_TO_INSTALL
-#  $EXTRA_OBJECTS_TO_CLEAN
-# and put in a directory where there is a .depend file.
-
-OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@
-OCAMLPATH = @OCAMLFIND_META_DIR@
-
-PREPROCOPTIONS = -pp camlp4o
-SYNTAXOPTIONS = -syntax camlp4o
-PREREQ =
-OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread
-OCAMLDEBUGOPTIONS = -g
-OCAMLARCHIVEOPTIONS =
-OCAMLFIND = OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH @OCAMLFIND@
-REQUIRES := $(shell $(OCAMLFIND) -query -format '%(requires)' helm-$(PACKAGE))
-OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS) $(PREPROCOPTIONS)
-OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) $(PREPROCOPTIONS)
-OCAMLDEP = $(OCAMLFIND) ocamldep -package "camlp4 $(CAMLP4REQUIRES)" $(SYNTAXOPTIONS) $(OCAMLDEPOPTIONS) 
-OCAMLLEX = ocamllex
-OCAMLYACC = ocamlyacc
-
-OCAMLC_P4 = $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS) $(SYNTAXOPTIONS)
-OCAMLOPT_P4 = $(OCAMLFIND) opt $(OCAMLOPTIONS) $(SYNTAXOPTIONS)
-
-LIBRARIES = $(shell $(OCAMLFIND) query -recursive -predicates "byte $(PREDICATES)" -format "%d/%a" $(REQUIRES))
-LIBRARIES_OPT = $(shell $(OCAMLFIND) query -recursive -predicates "native $(PREDICATES)" -format "%d/%a" $(REQUIRES))
-LIBRARIES_DEPS = \
-	$(foreach X,$(filter-out /usr/lib/ocaml%,$(LIBRARIES)),\
-		$(wildcard \
-			$(shell dirname $(X))/*.mli \
-			$(shell dirname $(X))/*.ml \
-			$(shell dirname $(X))/paramodulation/*.ml \
-			$(shell dirname $(X))/paramodultation/*.mli))
-
-
-ARCHIVE = $(PACKAGE).cma
-ARCHIVE_OPT = $(PACKAGE).cmxa
-OBJECTS_TO_INSTALL = $(ARCHIVE) $(ARCHIVE_OPT) $(ARCHIVE_OPT:%.cmxa=%.a) \
-                     $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.cmi) \
-                     $(EXTRA_OBJECTS_TO_INSTALL)
-DEPEND_FILES = $(INTERFACE_FILES) $(IMPLEMENTATION_FILES)
-
-$(ARCHIVE): $(IMPLEMENTATION_FILES:%.ml=%.cmo) $(LIBRARIES)
-	$(H)if [ $(PACKAGE) != dummy ]; then \
-	echo "  OCAMLC -a $@";\
-	$(OCAMLC) $(OCAMLARCHIVEOPTIONS) -a -o $@ \
-		$(IMPLEMENTATION_FILES:%.ml=%.cmo); fi
-
-$(ARCHIVE_OPT): $(IMPLEMENTATION_FILES:%.ml=%.cmx) $(LIBRARIES_OPT)
-	$(H)if [ $(PACKAGE) != dummy ]; then \
-	echo "  OCAMLOPT -a $@";\
-	$(OCAMLOPT) $(OCAMLARCHIVEOPTIONS) -a -o $@ \
-		$(IMPLEMENTATION_FILES:%.ml=%.cmx); fi
-
-prereq: $(PREREQ)
-all: prereq $(IMPLEMENTATION_FILES:%.ml=%.cmo) $(ARCHIVE)
-	@echo -n 
-opt: prereq $(IMPLEMENTATION_FILES:%.ml=%.cmx) $(ARCHIVE_OPT)
-	@echo -n 
-world: all opt
-test: test.ml $(ARCHIVE)
-	$(OCAMLC) $(ARCHIVE) -linkpkg -o $@ $<
-test.opt: test.ml $(ARCHIVE_OPT)
-	$(OCAMLOPT) $(ARCHIVE_OPT) -linkpkg -o $@ $<
-
-depend: $(DEPEND_FILES)
-	$(OCAMLDEP) $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend
-
-$(PACKAGE).ps: .dep.dot
-	dot -Tps -o $@ $<
-
-.dep.dot: .depend
-	ocamldot < .depend > $@
-
-%.cmi: %.mli
-	@echo "  OCAMLC $<"
-	$(H)$(OCAMLC) -c $<
-%.cmo %.cmi: %.ml
-	@echo "  OCAMLC $<"
-	$(H)$(OCAMLC) -c $<
-%.cmx: %.ml
-	@echo "  OCAMLOPT $<"
-	$(H)$(OCAMLOPT) -c $<
-%.annot: %.ml
-	$(OCAMLC) -dtypes $(PKGS) -c $<
-%.ml %.mli: %.mly
-	$(OCAMLYACC) $<
-%.ml: %.mll
-	$(OCAMLLEX) $<
-
-$(IMPLEMENTATION_FILES:%.ml=%.cmo): $(LIBRARIES)
-$(IMPLEMENTATION_FILES:%.ml=%.cmi): $(LIBRARIES_DEPS)
-$(IMPLEMENTATION_FILES:%.ml=%.cmx): $(LIBRARIES_OPT)
-
-clean:
-	rm -f *.cm[ioax] *.cmxa *.o *.a *.annot $(EXTRA_OBJECTS_TO_CLEAN)
-	if [ -f test ]; then rm -f test; else true; fi
-	if [ -f test.opt ]; then rm -f test.opt; else true; fi
-
-install:
-	mkdir $(OCAMLFIND_DEST_DIR)/$(PACKAGE)
-	cp $(OBJECTS_TO_INSTALL) $(OCAMLFIND_DEST_DIR)/$(PACKAGE)
-
-uninstall:
-	cd $(OCAMLFIND_DEST_DIR)/$(PACKAGE) && rm -f $(OBJECTS_TO_INSTALL)
-	rmdir $(OCAMLFIND_DEST_DIR)/$(PACKAGE)
-
-backup:
-	cd ..; tar cvzf $(PACKAGE)_$(shell date +%s).tar.gz $(PACKAGE)
-
-ocamlinit:
-	echo "#use \"topfind\";;" > .ocamlinit
-	echo "#thread;;" >> .ocamlinit
-	for p in $(REQUIRES); do echo "#require \"$$p\";;" >> .ocamlinit; done
-	echo "#load \"$(PACKAGE).cma\";;" >> .ocamlinit
-
-# $(STATS_EXCLUDE) may be defined in libraries' Makefile to exclude some file
-# from statistics collection
-STATS_FILES = \
-	$(shell find . -maxdepth 1 -type f -name \*.ml $(foreach f,$(STATS_EXCLUDE),-not -name $(f))) \
-	$(shell find . -maxdepth 1 -type f -name \*.mli $(foreach f,$(STATS_EXCLUDE),-not -name $(f)))
-.stats: $(STATS_FILES)
-	rm -f .stats
-	echo -n "LOC:" >> .stats
-	wc -l $(STATS_FILES) | tail -1 | awk '{ print $$1 }' >> .stats
-
-.PHONY: all opt world backup depend install uninstall clean ocamlinit
-
-ifneq ($(MAKECMDGOALS), depend)
-   include .depend   
-endif
-
-NULL =
-
diff --git a/helm/ocaml/Makefile.defs.in b/helm/ocaml/Makefile.defs.in
deleted file mode 100644
index a3681d0c5..000000000
--- a/helm/ocaml/Makefile.defs.in
+++ /dev/null
@@ -1 +0,0 @@
-OCAMLFIND = OCAMLPATH=@OCAMLPATH@ @OCAMLFIND@
diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in
deleted file mode 100644
index 7ab72ed24..000000000
--- a/helm/ocaml/Makefile.in
+++ /dev/null
@@ -1,132 +0,0 @@
-
-export SHELL=/bin/bash
-
-# Warning: the modules must be in compilation order
-NULL =
-MODULES =			\
-	extlib			\
-	xml			\
-	hgdome			\
-	registry		\
- 	hmysql 			\
-	utf8_macros		\
-	thread			\
-	xmldiff			\
-	urimanager		\
-	logger			\
-	getter			\
-	cic			\
-	cic_proof_checking	\
-	cic_acic		\
-	acic_content		\
-	content_pres		\
-	grafite			\
-	metadata		\
-	library			\
-	cic_unification		\
-	whelp			\
-	tactics			\
-	cic_disambiguation	\
-	lexicon			\
-	grafite_engine          \
-	grafite_parser          \
-	tactics/paramodulation 	\
-	$(NULL)
-
-OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@
-OCAMLPATH = @OCAMLFIND_META_DIR@
-OCAMLFIND = OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH @OCAMLFIND@
-
-METAS = $(filter-out %/paramodulation,$(MODULES:%=METAS/META.helm-%))
-
-all: metas $(MODULES:%=%.all) 
-opt: metas $(MODULES:%=%.opt)
-world: all opt
-metas: $(METAS)
-depend: $(MODULES:%=%.depend)
-install: $(MODULES:%=%.install)
-uninstall: $(MODULES:%=%.uninstall)
-clean: $(MODULES:%=%.clean) clean_metas
-
-.stats: $(MODULES:%=%.stats)
-	(for m in $(MODULES); do echo -n "$$m:"; cat $$m/.stats; done) \
-	 | sort -t : -k 2 -n -r > .stats
-
-EXTRA_DIST_CLEAN = \
-	libraries-clusters.ps 	\
-	libraries-clusters.pdf 	\
-	libraries-ext.ps 	\
-	libraries.ps 		\
-	.dep.dot 		\
-	.extdep.dot 		\
-	.clustersdep.dot 	\
-	$(NULL)
-
-clean_metas:
-	rm -f $(METAS)
-distclean: clean clean_metas
-	rm -f configure config.log config.cache config.status
-	rm -f Makefile Makefile.common $(EXTRA_DIST_CLEAN)
-
-.PHONY: all opt world metas depend install uninstall clean clean_metas distclean
-
-%.all:
-	@OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* all 
-%.opt:
-	@OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* opt
-%.clean:
-	@OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* clean 
-%.depend:
-	@OCAMLPATH=$(OCAMLPATH):$$OCAMLPATH $(MAKE) -C $* depend 
-%.stats:
-	@$(MAKE) -C $* .stats
-
-$(MODULES:%=%.install):
-	cd $(@:%.install=%) && make install
-	export TARGET=$(OCAMLFIND_META_DIR)/$(@:%.install=META.helm-%) ; \
-	cp METAS/$(@:%.install=meta.helm-%.src) $$TARGET && \
-	echo "directory=\"$(OCAMLFIND_DEST_DIR)/$(@:%.install=%)\"" >> $$TARGET
-$(MODULES:%=%.uninstall):
-	cd $(@:%.uninstall=%) && make uninstall
-	rm -f $(OCAMLFIND_META_DIR)/$(@:%.uninstall=META.helm-%)
-METAS/META.helm-%: METAS/meta.helm-%.src
-	cp $< $@ && echo "directory=\"$(shell pwd)/$*\"" >> $@
-
-.PHONY: .dep.dot
-.dep.dot:
-	echo "digraph G {" > $@
-	echo "   rankdir = TB ;" >> $@
-	for i in $(MODULES); do $(OCAMLFIND) query helm-$$i -recursive -p-format | grep helm | sed "s/^helm-/ \"$$i\" -> \"/g" | sed "s/$$/\";/g" >> $@ ; done
-	mv $@ $@.old ; ./simplify_deps/simplify_deps.opt < $@.old > $@ ; rm $@.old
-	echo "}" >> $@
-
-.PHONY: .alldep.dot
-.alldep.dot:
-	echo "digraph G {" > $@
-	echo "   rankdir = TB ;" >> $@
-	for i in $(MODULES); do $(OCAMLFIND) query helm-$$i -recursive -p-format | grep -v "pxp-" | sed "s/^pxp/pxp[-*]/g" | sed "s/^/ \"helm-$$i\" -> \"/g" | sed "s/$$/\";/g" >> $@ ; done
-	mv $@ $@.old ; ./simplify_deps/simplify_deps.opt < $@.old > $@ ; rm $@.old
-	for i in $(MODULES); do echo "\"helm-$$i\" [shape=box,style=filled,fillcolor=yellow];" >> $@ ; done
-	echo "}" >> $@
-
-.extdep.dot: .dep.dot
-	STATS/patch_deps.sh $< $@
-.clustersdep.dot: .dep.dot
-	USE_CLUSTERS=yes STATS/patch_deps.sh $< $@
-
-libraries.ps: .dep.dot
-	dot -Tps -o $@ $<
-libraries-ext.ps: .extdep.dot
-	dot -Tps -o $@ $<
-libraries-clusters.ps: .clustersdep.dot
-	dot -Tps -o $@ $<
-libraries-complete.ps: .alldep.dot
-	dot -Tps -o $@ $<
-
-ps: libraries.ps libraries-ext.ps libraries-clusters.ps
-
-tags: TAGS
-.PHONY: TAGS
-TAGS:
-	otags -vi -r .
-
diff --git a/helm/ocaml/acic_content/Makefile b/helm/ocaml/acic_content/Makefile
index cc4da3781..862a9eefb 100644
--- a/helm/ocaml/acic_content/Makefile
+++ b/helm/ocaml/acic_content/Makefile
@@ -16,4 +16,5 @@ IMPLEMENTATION_FILES =		\
 	cicNotationPt.ml	\
 	$(INTERFACE_FILES:%.mli=%.ml)
 
+include ../../Makefile.defs
 include ../Makefile.common
diff --git a/helm/ocaml/cic/Makefile b/helm/ocaml/cic/Makefile
index 4e36af019..f3d9df425 100644
--- a/helm/ocaml/cic/Makefile
+++ b/helm/ocaml/cic/Makefile
@@ -16,4 +16,5 @@ IMPLEMENTATION_FILES = \
 EXTRA_OBJECTS_TO_INSTALL = cic.ml cic.cmi
 EXTRA_OBJECTS_TO_CLEAN =
 
+include ../../Makefile.defs
 include ../Makefile.common
diff --git a/helm/ocaml/cic_acic/Makefile b/helm/ocaml/cic_acic/Makefile
index a7f1e19cf..2669afb11 100644
--- a/helm/ocaml/cic_acic/Makefile
+++ b/helm/ocaml/cic_acic/Makefile
@@ -9,4 +9,5 @@ INTERFACE_FILES =		\
 	$(NULL)
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 
+include ../../Makefile.defs
 include ../Makefile.common
diff --git a/helm/ocaml/cic_disambiguation/Makefile b/helm/ocaml/cic_disambiguation/Makefile
index 9c231dd87..cd03e8281 100644
--- a/helm/ocaml/cic_disambiguation/Makefile
+++ b/helm/ocaml/cic_disambiguation/Makefile
@@ -15,7 +15,9 @@ clean:
 distclean:
 	rm -f macro_table.dump
 
+include ../../Makefile.defs
 include ../Makefile.common
+
 OCAMLARCHIVEOPTIONS += -linkall
 
 disambiguateTypes.cmi: disambiguateTypes.mli
diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile
index bb9647926..8e2f99a15 100644
--- a/helm/ocaml/cic_proof_checking/Makefile
+++ b/helm/ocaml/cic_proof_checking/Makefile
@@ -23,6 +23,7 @@ EXTRA_OBJECTS_TO_INSTALL = \
             cicMiniReduction.cmo cicMiniReduction.cmx cicMiniReduction.o
 EXTRA_OBJECTS_TO_CLEAN =
 
+include ../../Makefile.defs
 include ../Makefile.common
 
 cicReduction.cmo: OCAMLOPTIONS+=-rectypes
diff --git a/helm/ocaml/cic_proof_checking/utilities/Makefile b/helm/ocaml/cic_proof_checking/utilities/Makefile
index 174546634..383391d70 100644
--- a/helm/ocaml/cic_proof_checking/utilities/Makefile
+++ b/helm/ocaml/cic_proof_checking/utilities/Makefile
@@ -2,8 +2,8 @@ UTILITIES = create_environment parse_library list_uris
 UTILITIES_OPT = $(patsubst %,%.opt,$(UTILITIES))
 LINKOPTS = -linkpkg -thread
 LIBS = helm-cic_proof_checking
-OCAMLC = ocamlfind ocamlc $(LINKOPTS) -package $(LIBS)
-OCAMLOPT = ocamlfind opt $(LINKOPTS) -package $(LIBS)
+OCAMLC = $(OCAMLFIND) ocamlc $(LINKOPTS) -package $(LIBS)
+OCAMLOPT = $(OCAMLFIND) opt $(LINKOPTS) -package $(LIBS)
 all: $(UTILITIES)
 	@echo -n
 opt: $(UTILITIES_OPT)
@@ -17,3 +17,5 @@ opt: $(UTILITIES_OPT)
 clean:
 	rm -f $(UTILITIES) $(UTILITIES_OPT) *.cm[iox] *.o
 
+include ../../../Makefile.defs
+
diff --git a/helm/ocaml/cic_unification/Makefile b/helm/ocaml/cic_unification/Makefile
index 3db00fe5c..62be3a61c 100644
--- a/helm/ocaml/cic_unification/Makefile
+++ b/helm/ocaml/cic_unification/Makefile
@@ -9,4 +9,5 @@ INTERFACE_FILES = \
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 EXTRA_OBJECTS_TO_INSTALL =
 
+include ../../Makefile.defs
 include ../Makefile.common
diff --git a/helm/ocaml/configure.ac b/helm/ocaml/configure.ac
deleted file mode 100644
index ec6498a7b..000000000
--- a/helm/ocaml/configure.ac
+++ /dev/null
@@ -1,55 +0,0 @@
-AC_INIT(Makefile.in)
-
-AC_CHECK_PROG(HAVE_OCAMLC, ocamlc, yes, no)
-if test $HAVE_OCAMLC = "no"; then
-  AC_MSG_ERROR(could not find ocamlc in PATH, please make sure ocaml is installed)
-fi
-
-AC_CHECK_PROG(HAVE_OCAMLFIND, ocamlfind, yes, no)
-if test $HAVE_OCAMLFIND = "no"; then
-  AC_MSG_ERROR(could not find ocamlfind in PATH, please make sure findlib is installed)
-else
-  OCAMLFIND=ocamlfind
-fi
-
-OCAMLFIND_COMMANDS=""
-AC_CHECK_PROG(HAVE_OCAMLC_OPT, ocamlc.opt, yes, no)
-if test $HAVE_OCAMLC_OPT = "yes"; then
-  if test "$OCAMLFIND_COMMANDS" = ""; then
-    OCAMLFIND_COMMANDS="ocamlc=ocamlc.opt"
-  else
-    OCAMLFIND_COMMANDS="$OCAMLFIND_COMMANDS ocamlc=ocamlc.opt"
-  fi
-fi
-AC_CHECK_PROG(HAVE_OCAMLOPT_OPT, ocamlopt.opt, yes, no)
-if test $HAVE_OCAMLOPT_OPT = "yes"; then
-  if test "$OCAMLFIND_COMMANDS" = ""; then
-    OCAMLFIND_COMMANDS="ocamlopt=ocamlopt.opt"
-  else
-    OCAMLFIND_COMMANDS="$OCAMLFIND_COMMANDS ocamlopt=ocamlopt.opt"
-  fi
-fi
-AC_CHECK_PROG(HAVE_OCAMLDEP_OPT, ocamldep.opt, yes, no)
-if test $HAVE_OCAMLDEP_OPT = "yes"; then
-  if test "$OCAMLFIND_COMMANDS" = ""; then
-    OCAMLFIND_COMMANDS="ocamldep=ocamldep.opt"
-  else
-    OCAMLFIND_COMMANDS="$OCAMLFIND_COMMANDS ocamldep=ocamldep.opt"
-  fi
-fi
-if test "$OCAMLFIND_COMMANDS" != ""; then
-  OCAMLFIND="OCAMLFIND_COMMANDS='$OCAMLFIND_COMMANDS' $OCAMLFIND"
-fi
-
-AC_MSG_CHECKING("where to install the META files")
-OCAMLFIND_META_DIR=`pwd`/METAS
-AC_MSG_RESULT($OCAMLFIND_META_DIR)
-
-AC_SUBST(OCAMLFIND)
-AC_SUBST(OCAMLFIND_META_DIR)
-
-AC_OUTPUT([
-  Makefile
-  Makefile.common
-])
-
diff --git a/helm/ocaml/content_pres/Makefile b/helm/ocaml/content_pres/Makefile
index 459b793f0..0cd8b4226 100644
--- a/helm/ocaml/content_pres/Makefile
+++ b/helm/ocaml/content_pres/Makefile
@@ -40,6 +40,7 @@ cicNotationParser.cmx: OCAMLOPT = $(OCAMLOPT_P4)
 cicNotationLexer.ml.annot: OCAMLC = $(OCAMLC_P4)
 cicNotationParser.ml.annot: OCAMLC = $(OCAMLC_P4)
 
+include ../../Makefile.defs
 include ../Makefile.common
 
 # <cross> cross compatibility among ocaml 3.09 and ocaml 3.08, to be removed as
diff --git a/helm/ocaml/extlib/Makefile b/helm/ocaml/extlib/Makefile
index c67778af4..d2e5cddf6 100644
--- a/helm/ocaml/extlib/Makefile
+++ b/helm/ocaml/extlib/Makefile
@@ -13,4 +13,5 @@ IMPLEMENTATION_FILES = \
 EXTRA_OBJECTS_TO_INSTALL =
 EXTRA_OBJECTS_TO_CLEAN =
 
+include ../../Makefile.defs
 include ../Makefile.common
diff --git a/helm/ocaml/getter/Makefile b/helm/ocaml/getter/Makefile
index 9ebca237a..0f2132eec 100644
--- a/helm/ocaml/getter/Makefile
+++ b/helm/ocaml/getter/Makefile
@@ -16,5 +16,6 @@ IMPLEMENTATION_FILES = \
 	http_getter_types.ml \
 	$(INTERFACE_FILES:%.mli=%.ml)
 
+include ../../Makefile.defs
 include ../Makefile.common
 
diff --git a/helm/ocaml/grafite/Makefile b/helm/ocaml/grafite/Makefile
index 182cd4561..6eb3e7a78 100644
--- a/helm/ocaml/grafite/Makefile
+++ b/helm/ocaml/grafite/Makefile
@@ -10,4 +10,5 @@ IMPLEMENTATION_FILES =		\
 	$(INTERFACE_FILES:%.mli=%.ml)
 
 
+include ../../Makefile.defs
 include ../Makefile.common
diff --git a/helm/ocaml/grafite_engine/Makefile b/helm/ocaml/grafite_engine/Makefile
index e72acd29c..d810e1be2 100644
--- a/helm/ocaml/grafite_engine/Makefile
+++ b/helm/ocaml/grafite_engine/Makefile
@@ -9,4 +9,5 @@ INTERFACE_FILES = \
 	$(NULL)
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 
+include ../../Makefile.defs
 include ../Makefile.common
diff --git a/helm/ocaml/grafite_parser/Makefile b/helm/ocaml/grafite_parser/Makefile
index 25896da87..8482825a6 100644
--- a/helm/ocaml/grafite_parser/Makefile
+++ b/helm/ocaml/grafite_parser/Makefile
@@ -42,4 +42,5 @@ test_dep: test_dep.ml $(PACKAGE).cma
 	@echo "  OCAMLC $<"
 	@$(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $<
 
+include ../../Makefile.defs
 include ../Makefile.common
diff --git a/helm/ocaml/hbugs/Makefile b/helm/ocaml/hbugs/Makefile
index c38ac3e92..4170d8081 100644
--- a/helm/ocaml/hbugs/Makefile
+++ b/helm/ocaml/hbugs/Makefile
@@ -24,6 +24,7 @@ INTERFACE_FILES = \
 	hbugs_types.mli \
 	$(patsubst %.ml, %.mli, $(IMPLEMENTATION_FILES))
 
+include ../../Makefile.defs
 include ../Makefile.common
 include .tutors.ml
 include .generated_tutors.ml
diff --git a/helm/ocaml/hgdome/Makefile b/helm/ocaml/hgdome/Makefile
index a7bb4dbb6..9630da26a 100644
--- a/helm/ocaml/hgdome/Makefile
+++ b/helm/ocaml/hgdome/Makefile
@@ -8,4 +8,5 @@ INTERFACE_FILES =		\
 
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 
+include ../../Makefile.defs
 include ../Makefile.common
diff --git a/helm/ocaml/hmysql/Makefile b/helm/ocaml/hmysql/Makefile
index 2ae1d4e59..8a83eb23e 100644
--- a/helm/ocaml/hmysql/Makefile
+++ b/helm/ocaml/hmysql/Makefile
@@ -8,4 +8,5 @@ IMPLEMENTATION_FILES = \
 EXTRA_OBJECTS_TO_INSTALL =
 EXTRA_OBJECTS_TO_CLEAN =
 
+include ../../Makefile.defs
 include ../Makefile.common
diff --git a/helm/ocaml/lexicon/Makefile b/helm/ocaml/lexicon/Makefile
index 0e9c09526..b8582baca 100644
--- a/helm/ocaml/lexicon/Makefile
+++ b/helm/ocaml/lexicon/Makefile
@@ -14,4 +14,5 @@ IMPLEMENTATION_FILES =		\
 	$(INTERFACE_FILES:%.mli=%.ml)
 
 
+include ../../Makefile.defs
 include ../Makefile.common
diff --git a/helm/ocaml/library/Makefile b/helm/ocaml/library/Makefile
index 74a61aed5..4f0ca3eb8 100644
--- a/helm/ocaml/library/Makefile
+++ b/helm/ocaml/library/Makefile
@@ -16,4 +16,5 @@ INTERFACE_FILES = \
 IMPLEMENTATION_FILES = \
 	$(INTERFACE_FILES:%.mli=%.ml)
 
+include ../../Makefile.defs
 include ../Makefile.common
diff --git a/helm/ocaml/logger/Makefile b/helm/ocaml/logger/Makefile
index dab9f5cb3..39d690084 100644
--- a/helm/ocaml/logger/Makefile
+++ b/helm/ocaml/logger/Makefile
@@ -5,5 +5,6 @@ INTERFACE_FILES = \
 IMPLEMENTATION_FILES = \
 	$(INTERFACE_FILES:%.mli=%.ml)
 
+include ../../Makefile.defs
 include ../Makefile.common
 
diff --git a/helm/ocaml/metadata/Makefile b/helm/ocaml/metadata/Makefile
index 0a2496451..d02d021a5 100644
--- a/helm/ocaml/metadata/Makefile
+++ b/helm/ocaml/metadata/Makefile
@@ -12,6 +12,7 @@ IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 EXTRA_OBJECTS_TO_INSTALL =
 EXTRA_OBJECTS_TO_CLEAN =
 
+include ../../Makefile.defs
 include ../Makefile.common
 
 all: all_table_creator all_extractor
diff --git a/helm/ocaml/metadata/extractor/Makefile b/helm/ocaml/metadata/extractor/Makefile
index 7c2aec0e5..579a5655f 100644
--- a/helm/ocaml/metadata/extractor/Makefile
+++ b/helm/ocaml/metadata/extractor/Makefile
@@ -1,4 +1,3 @@
-OCAMLFIND=ocamlfind
 
 all: extractor extractor_manager 
 	@echo -n
@@ -34,3 +33,4 @@ export: extractor.opt extractor_manager.opt
 		./extractor_manager.opt 1>export.out 2>export.err
 	
 include .depend
+include ../../../Makefile.defs
diff --git a/helm/ocaml/metadata/table_creator/Makefile b/helm/ocaml/metadata/table_creator/Makefile
index 06335681c..c54e52d4a 100644
--- a/helm/ocaml/metadata/table_creator/Makefile
+++ b/helm/ocaml/metadata/table_creator/Makefile
@@ -1,5 +1,4 @@
 REQUIRES = mysql helm-metadata
-OCAMLFIND = ocamlfind
 
 INTERFACE_FILES = 
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) 
@@ -33,3 +32,4 @@ clean:
 	rm -f table_creator table_creator.opt table_destructor table_destructor.opt
 
 include .depend
+include ../../../Makefile.defs
diff --git a/helm/ocaml/registry/Makefile b/helm/ocaml/registry/Makefile
index 4d3e0a52c..bb9715ab4 100644
--- a/helm/ocaml/registry/Makefile
+++ b/helm/ocaml/registry/Makefile
@@ -3,5 +3,6 @@ PACKAGE = registry
 INTERFACE_FILES = helm_registry.mli
 IMPLEMENTATION_FILES = helm_registry.ml
 
+include ../../Makefile.defs
 include ../Makefile.common
 
diff --git a/helm/ocaml/tactics/Makefile b/helm/ocaml/tactics/Makefile
index db8cc9231..c7bf44694 100644
--- a/helm/ocaml/tactics/Makefile
+++ b/helm/ocaml/tactics/Makefile
@@ -28,6 +28,7 @@ tactics.mli: tactics.ml *Tactics.mli *Tactic.mli fourierR.mli ring.mli paramodul
 
 STATS_EXCLUDE = tactics.mli
 
+include ../../Makefile.defs
 include ../Makefile.common
 
 OCAMLOPTIONS+= -I paramodulation
diff --git a/helm/ocaml/tactics/paramodulation/Makefile b/helm/ocaml/tactics/paramodulation/Makefile
index ba8bd40aa..f1b613400 100644
--- a/helm/ocaml/tactics/paramodulation/Makefile
+++ b/helm/ocaml/tactics/paramodulation/Makefile
@@ -2,6 +2,7 @@ PACKAGE = dummy
 
 LOCALLINKOPTS = -package helm-cic_disambiguation,helm-content_pres,helm-grafite,helm-grafite_parser,helm-tactics
 
+include ../../../Makefile.defs
 include ../../Makefile.common
 
 all $(PACKAGE).cma :saturate 
diff --git a/helm/ocaml/thread/Makefile b/helm/ocaml/thread/Makefile
index db722abaa..46f009e07 100644
--- a/helm/ocaml/thread/Makefile
+++ b/helm/ocaml/thread/Makefile
@@ -6,6 +6,7 @@ IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 all: thread_fake.cma
 opt: thread_fake.cmxa
 
+include ../../Makefile.defs
 include ../Makefile.common
 
 fake/threadSafe.cmi: fake/threadSafe.mli
diff --git a/helm/ocaml/urimanager/Makefile b/helm/ocaml/urimanager/Makefile
index afd7d4442..592c0854e 100644
--- a/helm/ocaml/urimanager/Makefile
+++ b/helm/ocaml/urimanager/Makefile
@@ -6,4 +6,5 @@ IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 EXTRA_OBJECTS_TO_INSTALL =
 EXTRA_OBJECTS_TO_CLEAN =
 
+include ../../Makefile.defs
 include ../Makefile.common
diff --git a/helm/ocaml/utf8_macros/Makefile b/helm/ocaml/utf8_macros/Makefile
index 952b9f597..2b737627f 100644
--- a/helm/ocaml/utf8_macros/Makefile
+++ b/helm/ocaml/utf8_macros/Makefile
@@ -38,5 +38,6 @@ extra_clean:
 
 STATS_EXCLUDE = utf8MacroTable.ml
 
+include ../../Makefile.defs
 include ../Makefile.common
 
diff --git a/helm/ocaml/whelp/Makefile b/helm/ocaml/whelp/Makefile
index f43c77fa9..6d8d3958f 100644
--- a/helm/ocaml/whelp/Makefile
+++ b/helm/ocaml/whelp/Makefile
@@ -7,4 +7,5 @@ INTERFACE_FILES =	\
 
 IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 
+include ../../Makefile.defs
 include ../Makefile.common
diff --git a/helm/ocaml/xml/Makefile b/helm/ocaml/xml/Makefile
index 6ca7bd944..7948435aa 100644
--- a/helm/ocaml/xml/Makefile
+++ b/helm/ocaml/xml/Makefile
@@ -8,4 +8,5 @@ IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 EXTRA_OBJECTS_TO_INSTALL =
 EXTRA_OBJECTS_TO_CLEAN =
 
+include ../../Makefile.defs
 include ../Makefile.common
diff --git a/helm/ocaml/xmldiff/Makefile b/helm/ocaml/xmldiff/Makefile
index 62492069e..afffaeefb 100644
--- a/helm/ocaml/xmldiff/Makefile
+++ b/helm/ocaml/xmldiff/Makefile
@@ -6,4 +6,5 @@ IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml)
 EXTRA_OBJECTS_TO_INSTALL =
 EXTRA_OBJECTS_TO_CLEAN =
 
+include ../../Makefile.defs
 include ../Makefile.common