diff --git a/Makefile b/Makefile
index a80245c..d5aa0bf 100644
--- a/Makefile
+++ b/Makefile
@@ -1,15 +1,4 @@
-all: default doc
-default: Makefile.coq
-	make -f Makefile.coq
+# -*- Makefile -*-
 
-clean: Makefile.coq
-	make -f Makefile.coq clean
-	rm -f Makefile.coq
-
-install: Makefile.coq
-	make -f Makefile.coq install
-
-Makefile.coq: _CoqProject
-	coq_makefile -f _CoqProject -o Makefile.coq
-
-.PHONY: coq clean install doc
+# --------------------------------------------------------------------
+include Makefile.common
diff --git a/Makefile.common b/Makefile.common
new file mode 100644
index 0000000..c523410
--- /dev/null
+++ b/Makefile.common
@@ -0,0 +1,99 @@
+# -*- Makefile -*-
+
+######################################################################
+# USAGE:                                                             #
+# The rules this-config::, this-build::, this-distclean::,           #
+# pre-makefile::, this-clean:: and __always__:: may be extended      #
+# Additionally, the following variables may be customized:           #
+SUBDIRS?=
+COQBIN?=$(dir $(shell which coqtop))
+COQMAKEFILE?=$(COQBIN)coq_makefile
+COQDEP?=$(COQBIN)coqdep
+COQPROJECT?=_CoqProject
+COQMAKEOPTIONS?=
+COQMAKEFILEOPTIONS?=
+V?=
+VERBOSE?=V
+######################################################################
+
+# local context: -----------------------------------------------------
+.PHONY: all config build clean distclean __always__
+.SUFFIXES:
+
+H:= $(if $(VERBOSE),,@)  # not used yet
+TOP     = $(dir $(lastword $(MAKEFILE_LIST)))
+COQMAKE = $(MAKE) -f Makefile.coq $(COQMAKEOPTIONS)
+BRANCH_coq:= $(shell $(COQBIN)coqtop -v | head -1 | grep -E '(trunk|master)' \
+	      | wc -l | sed 's/ *//g')
+
+# coq version:
+ifneq "$(BRANCH_coq)" "0"
+COQVVV:= dev
+else
+COQVVV:=$(shell $(COQBIN)coqtop --print-version | cut -d" " -f1)
+endif
+
+COQV:= $(shell echo $(COQVVV) | cut -d"." -f1)
+COQVV:= $(shell echo $(COQVVV) | cut -d"." -f1-2)
+
+# all: ---------------------------------------------------------------
+all: config build
+
+# Makefile.coq: ------------------------------------------------------
+.PHONY: pre-makefile
+
+Makefile.coq: pre-makefile $(COQPROJECT) Makefile
+	$(COQMAKEFILE) $(COQMAKEFILEOPTIONS) -f $(COQPROJECT) -o Makefile.coq
+
+# Global config, build, clean and distclean --------------------------
+config: sub-config this-config
+
+build: sub-build this-build
+
+clean: sub-clean this-clean
+
+distclean: sub-distclean this-distclean
+
+# Local config, build, clean and distclean ---------------------------
+.PHONY: this-config this-build this-distclean this-clean
+
+this-config:: __always__
+
+this-build:: this-config Makefile.coq
+	+$(COQMAKE)
+
+this-distclean:: this-clean
+	rm -f Makefile.coq Makefile.coq.conf Makefile.coq
+
+this-clean:: __always__
+	@if [ -f Makefile.coq ]; then $(COQMAKE) cleanall; fi
+
+# Install target -----------------------------------------------------
+.PHONY: install
+
+install: __always__ Makefile.coq
+	$(COQMAKE) install
+# counting lines of Coq code -----------------------------------------
+.PHONY: count
+
+COQFILES = $(shell grep '.v$$' $(COQPROJECT))
+
+count:
+	@coqwc $(COQFILES) | tail -1 | \
+	  awk '{printf ("%d (spec=%d+proof=%d)\n", $$1+$$2, $$1, $$2)}'
+# Additionally cleaning backup (*~) files ----------------------------
+this-distclean::
+	rm -f $(shell find . -name '*~')
+
+# Make in SUBDIRS ----------------------------------------------------
+ifdef SUBDIRS
+sub-%: __always__
+	@set -e; for d in $(SUBDIRS); do +$(MAKE) -C $$d $(@:sub-%=%); done
+else
+sub-%: __always__
+	@true
+endif
+
+# Make of individual .vo ---------------------------------------------
+%.vo: __always__ Makefile.coq
+	+$(COQMAKE) $@
diff --git a/examples/Make b/examples/Make
new file mode 100644
index 0000000..05db16d
--- /dev/null
+++ b/examples/Make
@@ -0,0 +1,29 @@
+-Q . htt
+
+-arg -w -arg -notation-overridden
+-arg -w -arg -redundant-canonical-projection
+
+# release-specific arguments
+-arg -w -arg -notation-incompatible-prefix # specific to coq8.20.0 
+-arg -w -arg -deprecated-from-Coq # specific to coq8.21 
+-arg -w -arg -deprecated-dirpath-Coq # specific to coq8.21 
+
+exploit.v
+gcd.v
+counter.v
+llist.v
+dlist.v
+array.v
+queue.v
+cyclic.v
+stack.v
+bintree.v
+bst.v
+kvmaps.v
+hashtab.v
+bubblesort.v
+quicksort.v
+congmath.v
+congprog.v
+tree.v	
+union_find.v
diff --git a/examples/Makefile b/examples/Makefile
new file mode 100644
index 0000000..103b008
--- /dev/null
+++ b/examples/Makefile
@@ -0,0 +1,7 @@
+# -*- Makefile -*-
+
+# setting variables
+COQPROJECT?=Make
+
+# Main Makefile
+include ../Makefile.common
diff --git a/htt/Make b/htt/Make
new file mode 100644
index 0000000..dca3ca7
--- /dev/null
+++ b/htt/Make
@@ -0,0 +1,14 @@
+-Q . htt
+
+-arg -w -arg -notation-overridden
+-arg -w -arg -redundant-canonical-projection
+
+# release-specific arguments
+-arg -w -arg -notation-incompatible-prefix # specific to coq8.20.0 
+-arg -w -arg -deprecated-from-Coq # specific to coq8.21 
+-arg -w -arg -deprecated-dirpath-Coq # specific to coq8.21 
+
+options.v
+domain.v
+model.v
+heapauto.v
diff --git a/htt/Makefile b/htt/Makefile
new file mode 100644
index 0000000..103b008
--- /dev/null
+++ b/htt/Makefile
@@ -0,0 +1,7 @@
+# -*- Makefile -*-
+
+# setting variables
+COQPROJECT?=Make
+
+# Main Makefile
+include ../Makefile.common