5 files changed, 70 insertions, 5 deletions
diff --git a/dev/ci/README.md b/dev/ci/README.md
index 87f03aa99..dee3d2aff 100644
--- a/dev/ci/README.md
+++ b/dev/ci/README.md
@@ -96,7 +96,8 @@ PR by running GitLab CI on your private branches. To do so follow these steps:
 2. Click on "New Project".
 3. Choose "CI / CD for external repository" then click on "GitHub".
 4. Find your fork of the Coq repository and click on "Connect".
-5. You are encouraged to go to the CI / CD general settings and increase the
+5. If GitLab did not do so automatically, [enable the Container Registry](https://docs.gitlab.com/ee/user/project/container_registry.html#enable-the-container-registry-for-your-project).
+6. You are encouraged to go to the CI / CD general settings and increase the
    timeout from 1h to 2h for better reliability.
 
 Now everytime you push (including force-push unless you changed the default
@@ -137,3 +138,27 @@ Currently, available artifacts are:
 
 As an exception to the above, jobs testing that compilation triggers
 no OCaml warnings build Coq in parallel with other tests.
+
+### GitLab and Windows
+
+
+If your repository has access to runners tagged `windows`, setting the
+secret variable `WINDOWS` to `enabled` will add jobs building Windows
+versions of Coq (32bit and 64bit).
+
+The Windows jobs are enabled on Coq's repository, where pipelines for
+pull requests run.
+
+### GitLab and Docker
+
+System and opam packages are installed in a Docker image. The image is
+automatically built and uploaded to your GitLab registry, and is
+loaded by subsequent jobs.
+
+The Docker building job reuses the uploaded image if it is available,
+but if you wish to save more time you can skip the job by setting
+`SKIP_DOCKER` to `true`.
+
+This means you will need to change its value when the Docker image
+needs to be updated. You can do so for a single pipeline by starting
+it through the web interface.
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 03de1d53b..f867fd189 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -10,6 +10,10 @@ if [ -n "${GITLAB_CI}" ];
 then
     export COQBIN="$PWD/_install_ci/bin"
     export CI_BRANCH="$CI_COMMIT_REF_NAME"
+    if [[ ${CI_BRANCH#pr-} =~ ^[0-9]*$ ]]
+    then
+        export CI_PULL_REQUEST="${CI_BRANCH#pr-}"
+    fi
 else
     if [ -n "${TRAVIS}" ];
     then
diff --git a/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh
new file mode 100644
index 000000000..517088a24
--- /dev/null
+++ b/dev/ci/user-overlays/07213-ppedrot-fast-constr-match-no-context.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "7213" ] || [ "$CI_BRANCH" = "fast-constr-match-no-context" ]; then
+
+    ltac2_CI_BRANCH=fast-constr-match-no-context
+    ltac2_CI_GITURL=https://github.com/ppedrot/ltac2
+
+fi
diff --git a/dev/doc/MERGING.md b/dev/doc/MERGING.md
index 84ff94c66..a466124c1 100644
--- a/dev/doc/MERGING.md
+++ b/dev/doc/MERGING.md
@@ -109,9 +109,8 @@ There are two cases to consider:
 
 The merge script passes option `-S` to `git merge` to ensure merge commits
 are signed. Consequently, it depends on the GnuPG command utility being
-installed and a GPG key being available. Here is a short tutorial to
-creating your own GPG key:
-<https://ekaia.org/blog/2009/05/10/creating-new-gpgkey/>
+installed and a GPG key being available. Here is a short documentation on
+how to use GPG, git & GitHub: https://help.github.com/articles/signing-commits-with-gpg/.
 
 The script depends on a few other utilities. If you are a Nix user, the
 simplest way of getting them is to run `nix-shell` first.
diff --git a/dev/tools/coqdev.el b/dev/tools/coqdev.el
index 9dd12087a..70a9756e5 100644
--- a/dev/tools/coqdev.el
+++ b/dev/tools/coqdev.el
@@ -23,7 +23,7 @@
 
 ;; If you load this file from a git repository, checking out an old
 ;; commit will make it disappear and cause errors for your Emacs
-;; startup. To ignore those errors use (require 'coqdev nil t). If you
+;; startup.  To ignore those errors use (require 'coqdev nil t).  If you
 ;; check out a malicious commit Emacs startup would allow it to run
 ;; arbitrary code, to avoid this you can copy coqdev.el to any
 ;; location and adjust the load path accordingly (of course if you run
@@ -115,5 +115,36 @@ This does not enable `bug-reference-mode'."
       (setq-local bug-reference-url-format "https://github.com/coq/coq/issues/%s"))))
 (add-hook 'hack-local-variables-hook #'coqdev-setup-bug-reference-mode)
 
+(defun coqdev-sphinx-quote-coq-refman-region (left right &optional offset beg end)
+  "Add LEFT and RIGHT around the BEG..END.
+Leave the point after RIGHT.  BEG and END default to the bounds
+of the current region.  Leave point OFFSET characters after the
+left quote (if OFFSET is nil, leave the point after the right
+quote)."
+  (unless beg
+    (if (region-active-p)
+        (setq beg (region-beginning) end (region-end))
+      (setq beg (point) end nil)))
+  (save-excursion
+    (goto-char (or end beg))
+    (insert right))
+  (save-excursion
+    (goto-char beg)
+    (insert left))
+  (if (and end (not offset)) ;; Second test handles the ::`` case
+      (goto-char (+ end (length left) (length right)))
+    (goto-char (+ beg (or offset (length left))))))
+
+(defun coqdev-sphinx-rst-coq-action ()
+  "Insert a Sphinx role template or quote the current region."
+  (interactive)
+  (pcase (read-char "Command [gntm:`]?")
+    (?g (coqdev-sphinx-quote-coq-refman-region ":g:`" "`"))
+    (?n (coqdev-sphinx-quote-coq-refman-region ":n:`" "`"))
+    (?t (coqdev-sphinx-quote-coq-refman-region ":token:`" "`"))
+    (?m (coqdev-sphinx-quote-coq-refman-region ":math:`" "`"))
+    (?: (coqdev-sphinx-quote-coq-refman-region "::`" "`" 1))
+    (?` (coqdev-sphinx-quote-coq-refman-region "``" "``"))))
+
 (provide 'coqdev)
 ;;; coqdev ends here