diff --git a/.github/workflows/buid-documentation.yml b/.github/workflows/buid-documentation.yml
new file mode 100644
index 00000000..e2ed76ef
--- /dev/null
+++ b/.github/workflows/buid-documentation.yml
@@ -0,0 +1,72 @@
+name: Build LaTeX document and Coq-Doc
+
+on:
+  push:
+    branches:
+      - master
+  pull_request:
+    branches:
+      - '**'
+
+jobs:
+  build-pdf:
+    runs-on: ubuntu-latest
+    strategy:
+      matrix:
+        image:
+          - 'mathcomp/mathcomp:1.12.0-coq-8.13'
+      fail-fast: false
+    steps:
+      - name: Set up Git repository
+        uses: actions/checkout@v2
+
+      - name: Compile Coq-Doc
+        if: github.event_name == 'push' && github.ref == 'refs/heads/master'
+        uses: coq-community/docker-coq-action@v1
+        with:
+          custom_image: ${{ matrix.image }}
+          before_script: |
+            startGroup "Create Makefile.coq and add permission"
+              make || true
+              sudo chown -R coq:coq .
+            endGroup
+          script: |
+            startGroup "Build documentation"
+              make -j2 html
+            endGroup
+          uninstall: |
+            startGroup "Clean"
+              make clean
+            endGroup
+      - name: Revert Coq user permissions
+        # to avoid a warning at cleanup time
+        if: ${{ always() }}
+        run: sudo chown -R 1001:116 .
+
+      - name: Compile LaTeX document
+        uses: xu-cheng/latex-action@v2
+        with:
+          root_file: hydras.tex
+          working_directory: doc
+          latexmk_use_lualatex: true
+
+      - name: Extract PDF and Coq-Doc
+        run: |
+          mkdir -p public/doc public/theories
+          cp doc/hydras.pdf public/doc/
+          cp -r theories/html public/theories/ || true
+      # Depending on whether we are on master or not, we deploy to
+      # GitHub Pages or as an artifact
+      - name: Deploy to GitHub pages
+        if: github.event_name == 'push' && github.ref == 'refs/heads/master'
+        uses: crazy-max/ghaction-github-pages@v2
+        with:
+          build_dir: public
+          jekyll: false
+        env:
+          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
+      - name: Deploy artifact
+        if: github.event_name == 'pull_request' || github.ref != 'refs/heads/master'
+        uses: actions/upload-artifact@v2
+        with:
+          path: public
diff --git a/.github/workflows/build-pdf.yml b/.github/workflows/build-pdf.yml
deleted file mode 100644
index fc4edffd..00000000
--- a/.github/workflows/build-pdf.yml
+++ /dev/null
@@ -1,41 +0,0 @@
-name: Build LaTeX document
-
-on:
-  push:
-    branches:
-      - master
-  pull_request:
-    branches:
-      - '**'
-
-jobs:
-  build-pdf:
-    runs-on: ubuntu-latest
-    steps:
-      - name: Set up Git repository
-        uses: actions/checkout@v2
-      - name: Compile LaTeX document
-        uses: xu-cheng/latex-action@v2
-        with:
-          root_file: hydras.tex
-          working_directory: doc
-          latexmk_use_lualatex: true
-      - name: Extract PDF
-        run: |
-          mkdir -p public
-          cp doc/hydras.pdf public/
-      # Depending on whether we are on master or not, we deploy to
-      # GitHub Pages or as an artifact
-      - name: Deploy to GitHub pages
-        if: github.event_name == 'push' && github.ref == 'refs/heads/master'
-        uses: crazy-max/ghaction-github-pages@v2
-        with:
-          build_dir: public
-          jekyll: false
-        env:
-          GITHUB_TOKEN: ${{ secrets.GITHUB_TOKEN }}
-      - name: Deploy artifact
-        if: github.event_name == 'pull_request' || github.ref != 'refs/heads/master'
-        uses: actions/upload-artifact@v2
-        with:
-          path: public
diff --git a/README.md b/README.md
index b5e9f689..5f001969 100644
--- a/README.md
+++ b/README.md
@@ -71,11 +71,11 @@ This contribution contains two parts:
  ### Documentation
 
  Documentation for the `master` branch is continuously deployed at:
- https://coq-community.org/hydra-battles/hydras.pdf
+ https://coq-community.org/hydra-battles/doc/hydras.pdf
 
  The command `make pdf` generates a local copy as `doc/hydras.pdf`.
 
-##   Contents
+## Contents
 
 ###  coqdoc html files