diff --git a/doc/README.md b/doc/README.md
new file mode 100644
index 000000000..bcfb20aff
--- /dev/null
+++ b/doc/README.md
@@ -0,0 +1,60 @@
+# The structure of the documentation
+
+This directory contains the main Q*cert Web page, the Coq
+documentation in navigable form, and the Web demos.
+
+- `demo.html` is the old demo
+- `doc.html` contains a starting point for a _Commented Coq Development_ document that helps navigate the code
+- `index.html` is the Web site front page
+- `demo` is the full SIGMOD'2017 demo
+- `figure` is the LaTeX source and makefile for the compilation pipeline
+- `html` is the Coq code in navigable form produced by `coq2html`
+
+# To refresh the documentation
+
+If you make changes to the Coq code, you may want to re-generate the
+documentation.
+
+You will need a copy of `coq2html` checked out and compiled from the
+source. You can find `coq2html` at
+`https://github.com/xavierleroy/coq2html`. It's written in OCaml and
+should compile easily. Once compiled you need to move the produced
+`coq2html` executable into your PATH.
+
+Then from the top-level `qcert` direcory, do:
+
+```
+make qcert
+make documentation
+```
+
+This will regenerate the `./html` directory
+
+# To update the compilation pipeline
+
+Edit the LaTeX file `compiler-coq.tex`, then do:
+
+```
+cd figure
+make
+```
+
+# To deploy the demo and documentation
+
+To deploy the demo and new documentation to the external Q*cert Web
+site, first check that the `QUERYCERTDOTIO` has the right location for
+your checkout of the `querycert.github.io` project. By default, it's
+assumed to be checked out from github as a sibbling of the `qcert`
+repository.
+
+Then do:
+```
+make deploy
+```
+
+This will copy the main html files, the demos, and Coq documentation.
+
+You can then go to your `querycert.github.io` project and push the
+deployed changes to git, which will make the changes visible on the
+external Web site.
+