diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml
index cc69123..1296719 100644
--- a/.github/workflows/build.yml
+++ b/.github/workflows/build.yml
@@ -11,7 +11,7 @@ permissions:
 jobs:
 
   build:
-  
+
     runs-on: ubuntu-latest
 
     env:
@@ -52,3 +52,25 @@ jobs:
         # to avoid a warning at cleanup time
         if: ${{ always() }}
         run: sudo chown -R 1001:116 .  # <--
+
+      - name: Build doc overview
+        uses: docker://pandoc/core:2.9
+        with:
+          args: >-  # allows you to break string into multiple lines
+            --standalone
+            --output=docs/index.html
+            --css=coqdoc/resources/github-pandoc.css
+            --metadata title="LogRel Overview"
+            docs/index.md
+      - name: Setup Pages
+        if: github.ref_name == github.event.repository.default_branch
+        uses: actions/configure-pages@v3
+      - name: Upload artifact
+        if: github.ref_name == github.event.repository.default_branch
+        uses: actions/upload-pages-artifact@v1
+        with:
+          path: 'docs'
+      - name: Deploy to GitHub Pages
+        if: github.ref_name == github.event.repository.default_branch
+        id: deployment
+        uses: actions/deploy-pages@v1
diff --git a/.gitignore b/.gitignore
index 23a6318..2834be7 100644
--- a/.gitignore
+++ b/.gitignore
@@ -46,3 +46,7 @@ time-of-build-pretty.log
 
 Makefile.coq
 Makefile.coq.conf
+
+.DS_Store
+
+doc/coqdoc/*
diff --git a/Makefile b/Makefile
index 29336be..705607a 100644
--- a/Makefile
+++ b/Makefile
@@ -11,4 +11,9 @@ autosubst:
 	cd theories/autosubst ; \
 	$(MAKE) -f Makefile
 
+force _CoqProject Makefile: ;
+
+%: Makefile.coq force
+	@+$(MAKE) -f Makefile.coq $@
+
 .PHONY: all clean autosubst
diff --git a/Makefile.coq.local b/Makefile.coq.local
new file mode 100644
index 0000000..25df251
--- /dev/null
+++ b/Makefile.coq.local
@@ -0,0 +1,16 @@
+GLOBFILES = $(VFILES:.v=.glob)
+
+DOCDIR = doc
+COQDOCDIR = $(DOCDIR)/coqdoc
+
+COQDOCHTMLFLAGS = -toc --toc-depth 0 --no-lib-name --lib-subtitles --html \
+  --index indexpage --parse-comments -utf8
+
+coqdoc: $(GLOBFILES) $(VFILES) $(HEADER) $(FOOTER) $(RESOURCES) $(FRONTPAGE)
+	$(SHOW)'COQDOC -d $(COQDOCDIR)'
+	$(HIDE)mkdir -p $(COQDOCDIR)
+	$(HIDE)$(COQDOC) $(COQDOCHTMLFLAGS) $(COQDOCLIBS) -d $(COQDOCDIR) $(VFILES)
+.PHONY: coqdoc
+
+clean::
+	$(HIDE)rm -rf $(COQDOCDIR)/*.html
diff --git a/doc/index.md b/doc/index.md
new file mode 100644
index 0000000..5d6f332
--- /dev/null
+++ b/doc/index.md
@@ -0,0 +1,2 @@
+Formalisation of the "Dependent Ghosts Have a Reflection For Free" paper
+========================================================================