diff --git a/.gitignore b/.gitignore
index 6514860712fe52e0b1b5ce6c69491b7a34402bba..395ad7ae13832745adac0f59ba265f3f92f08a14 100644
--- a/.gitignore
+++ b/.gitignore
@@ -12,5 +12,6 @@ lia.cache
 Makefile.coq
 Makefile.coq.conf
 .Makefile.coq.d
+.coq-html.mk
 public/*
 _CoqProject
diff --git a/Makefile b/Makefile
index 19ac4e00fbb3825772d9fec83c0b65f98ea518c0..293a22c27a89559ce60966942b8a20de433e7c1f 100644
--- a/Makefile
+++ b/Makefile
@@ -1,49 +1,90 @@
-SRC := src
-MODULES := IntroElim \
-	   Laws \
-	   SomeExamples \
-	   Induction \
-	   Forall \
-	   Exists \
-	   Groups
-LIB := CoMoEx
-HTML := public
-
-VS := $(MODULES:%=$(SRC)/%.v)
+# Configuration
 
-.PHONY: all html coq clean clean_html clean_all
+PROJNAME = CoMoEx
+HTMLDIR = public/
+COMPONENTS := prop:PropLogic fol:FOL ind:Induction
 
-all: coq html _CoqProject
+COQDOC_FLAGS = --utf8
 
-html: coq $(SRC)
-	mkdir -p public
-	coqdoc -R $(SRC) $(LIB) $(VS) -d $(HTML) \
-		-utf8 --lib-name File --toc
+all: coq html _CoqProject
 
 coq: Makefile.coq
 	$(MAKE) -f Makefile.coq all
 
-clean: $(SRC)
-	rm -f $(SRC)/*.vo
-	rm -f $(SRC)/*.vok
-	rm -f $(SRC)/*.vos
-	rm -f $(SRC)/*.glob
-	rm -f $(SRC)/.*.aux
+Makefile.coq: _CoqProject Makefile
+	coq_makefile -f $< -o $@
+
+GENERATED_HTML = .coq-html.mk
+clean: Makefile.coq $(SRC)
+	$(MAKE) -f $< cleanall
 	rm -f Makefile.coq
 	rm -f Makefile.coq.conf
 	rm -f .Makefile.coq.d
 	rm -f _CoqProject
 
-clean_html: clean
-	rm -f -r $(HTML)
+clean_html: clean $(HTMLDIR)
+	rm -f $(GENERATED_HTML)
+	rm -f -r $(HTMLDIR)
 
 clean_all: clean clean_html
 
-$(SRC):
-	mkdir -p $(SRC)
+define GENCoqPr
+BEGIN { RS="[[:space:]]"; FS=":" }\
+{					\
+    dirname = $$1;					\
+    libname = $$2;					\
+    print "-R " dirname " " libname;			\
+    find = "find " dirname " -name '*.v' -maxdepth 1";	\
+    while ((find | getline) > 0) {			\
+	print;						\
+    }							\
+    close(find);					\
+}
+endef
 
 _CoqProject: Makefile
-	echo "-R $(SRC) $(LIB)\n\n$(SRC)" > _CoqProject
+	echo $(COMPONENTS) | awk '$(GENCoqPr)' > $@
+
+$(HTMLDIR):
+	mkdir -p $(HTMLDIR)
+
+html: $(HTMLDIR)/toc.html
 
-Makefile.coq: Makefile $(VS) $(SRC)
-	@coq_makefile -o Makefile.coq -R $(SRC) $(LIB) $(VS)
+define GENIndex
+BEGIN {									\
+    print "<html><body><h1>Table of Contents for $(PROJNAME)</h1>";	\
+}\
+{\
+	printf("<h2><a href=\"%s.html\">%s</a></h2>\n", $$1, $$1);\
+}
+endef
+
+$(HTMLDIR)/toc.html: $(HTMLDIR)
+	find $(HTMLDIR) -name '*.html' -print0 | xargs -0 basename -a -s .html | grep -Fxv 'toc' | sort | awk '$(GENIndex)' > $@
+
+define GENMakefile
+BEGIN { RS="[[:space:]]"; FS=":" }			\
+{							\
+    dirname = $$1;					\
+    libname = $$2;					\
+    find = "find " dirname " -name '*.v' -maxdepth 1";	\
+    while ((find | getline line) > 0) {			\
+       match(line, /\/([^\/]+).v/, part);		\
+       html = HTMLDIR libname "." part[1] ".html";	\
+       print html ": " line " " HTMLDIR;		\
+       print "\tcoqdoc -o $$@ $$< --lib-name $(PROJNAME) $(COQDOC_FLAGS)";\
+       htmls = htmls " " html;				\
+    }							\
+    close(find);					\
+}							\
+END {							\
+    print "html:" htmls;				\
+    print HTMLDIR "/toc.html: " htmls;		\
+}
+endef
+
+$(GENERATED_HTML): Makefile $(HTMLDIR)
+	echo $(COMPONENTS) | awk -v HTMLDIR="$(HTMLDIR)" '$(GENMakefile)' > $@
+-include $(GENERATED_HTML)
+
+.PHONY: all html coq clean clean_html clean_all
diff --git a/src/Exists.v b/fol/Exists.v
similarity index 100%
rename from src/Exists.v
rename to fol/Exists.v
diff --git a/src/Forall.v b/fol/Forall.v
similarity index 100%
rename from src/Forall.v
rename to fol/Forall.v
diff --git a/src/Groups.v b/fol/Groups.v
similarity index 100%
rename from src/Groups.v
rename to fol/Groups.v
diff --git a/src/Induction.v b/ind/Induction.v
similarity index 100%
rename from src/Induction.v
rename to ind/Induction.v
diff --git a/src/IntroElim.v b/prop/IntroElim.v
similarity index 100%
rename from src/IntroElim.v
rename to prop/IntroElim.v
diff --git a/src/Laws.v b/prop/Laws.v
similarity index 100%
rename from src/Laws.v
rename to prop/Laws.v
diff --git a/src/SomeExamples.v b/prop/SomeExamples.v
similarity index 98%
rename from src/SomeExamples.v
rename to prop/SomeExamples.v
index 99b6c5e30b0aac5599542b452d9754cd4bb27cdd..d3584517827d29211659876a3eec133c3194c608 100644
--- a/src/SomeExamples.v
+++ b/prop/SomeExamples.v
@@ -3,7 +3,7 @@ Require Import Classical_Prop.
 (** In diesem File habe ich versucht, eigene Beispiele zu kreieren. Wahrscheinlich wird insbesondere diese Sammlung mit der Zeit weiter ergänzt. **)
 
 (** Dank der folgenden Zeile stehen uns die bereits bewiesenen Gesetze aus Laws.v zur Verfügung: *)
-From CoMoEx Require Import Laws.
+From PropLogic Require Import Laws.
 
 (** Man kann z.B. `de_morgan_1` ganz normal aufrufen, wie in der folgenden Section zu sehen ist: *)