27 files changed, 199 insertions, 68 deletions
diff --git a/dev/build/windows/MakeCoq_trunk_installer.bat b/dev/build/windows/MakeCoq_master_installer.bat
index f4f5827328..72640d5d79 100755
--- a/dev/build/windows/MakeCoq_trunk_installer.bat
+++ b/dev/build/windows/MakeCoq_master_installer.bat
@@ -16,7 +16,7 @@ call MakeCoq_SetRootPath
 call MakeCoq_MinGW.bat ^
   -arch=64 ^
   -installer=Y ^
-  -coqver=git-trunk ^
+  -coqver=git-master ^
   -destcyg="%ROOTPATH%\cygwin_coq64_trunk_inst" ^
   -destcoq="%ROOTPATH%\coq64_trunk_inst"
 
diff --git a/dev/build/windows/makecoq_mingw.sh b/dev/build/windows/makecoq_mingw.sh
index 859b3e3166..963b0e6387 100755
--- a/dev/build/windows/makecoq_mingw.sh
+++ b/dev/build/windows/makecoq_mingw.sh
@@ -983,6 +983,15 @@ function make_ocaml {
       cp Changes      "$PREFIXOCAML/license_readme/ocaml/Changes.txt"
     fi
 
+    # Since 4.07 this library is part of ocaml
+    mkdir -p "$PREFIXOCAML/libocaml/site-lib/seq/"
+    cat > "$PREFIXOCAML/libocaml/site-lib/seq/META" <<EOT
+name="seq"
+version="[distributed with OCaml 4.07 or above]"
+description="dummy backward-compatibility package for iterators"
+requires=""
+EOT
+
     build_post
   fi
 }
@@ -1093,13 +1102,14 @@ function make_camlp5 {
   make_ocaml
   make_findlib
 
-  if build_prep https://github.com/camlp5/camlp5/archive rel707 tar.gz 1 camlp5-rel707; then
+  if build_prep https://github.com/camlp5/camlp5/archive rel711 tar.gz 1 camlp5-rel711; then
     logn configure ./configure
     # Somehow my virus scanner has the boot.new/SAVED directory locked after the move for a second => repeat until success
     sed -i 's/mv boot.new boot/until mv boot.new boot; do sleep 1; done/' Makefile
     # shellcheck disable=SC2086
     log1 make world.opt $MAKE_OPT
     log2 make install
+    cp lib/*.a "$PREFIXOCAML/libocaml/camlp5/"
     log2 make clean
     # For some reason META is not built / copied, but it is required
     log2 make -C etc META
@@ -1154,6 +1164,47 @@ function make_lablgtk {
   fi
 }
 
+##### Elpi #####
+
+function make_seq {
+  make_ocaml
+  # since 4.07 this package is part of ocaml
+
+}
+
+function make_re {
+  make_ocaml
+  make_dune
+  make_seq
+
+  if build_prep https://github.com/ocaml/ocaml-re/archive 1.9.0 tar.gz 1 ocaml-re; then
+
+    log2 dune build -p re
+    log2 dune install re
+
+    build_post
+  fi
+
+}
+
+function make_elpi {
+  make_ocaml
+  make_findlib
+  make_camlp5
+  make_dune
+  make_re
+
+  if build_prep https://github.com/LPCIC/elpi/archive v1.11.0 tar.gz; then
+
+    log2 make build DUNE_OPTS="-p elpi"
+    log2 make install DUNE_OPTS="-p elpi"
+
+    build_post
+
+  fi
+
+}
+
 ##### COQ #####
 
 # Copy one DLLfrom cygwin MINGW packages to Coq install folder
@@ -1904,6 +1955,36 @@ function make_addon_gappa {
   fi
 }
 
+# Elpi: extension language for Coq based. It lets one define commands in tactics
+# in a high level programming language with support for binders and unification
+# variables.
+
+function make_addon_elpi {
+  make_elpi
+  installer_addon_dependency elpi
+  if build_prep_overlay elpi ; then
+    installer_addon_section elpi "Elpi extension language" "Coq plugin for the Elpi extension language" ""
+    logn build make
+    logn installe make install
+    build_post
+  fi
+}
+
+# Hierarchy Builder: high level language to declare a hierarchy of structures
+# compiled down to records and canonical structures.
+
+function make_addon_HB {
+  installer_addon_dependency_beg elpi_hb
+  make_addon_elpi
+  installer_addon_dependency_end
+  if build_prep_overlay elpi_hb ; then
+    installer_addon_section elpi_hb "Hierarchy Builder" "Coq library to declare algebraic hierarchies" ""
+    logn build make
+    logn install make install VFILES=structures.v
+    build_post
+  fi
+}
+
 # Main function for building addons
 
 function make_addons {
diff --git a/dev/ci/README-developers.md b/dev/ci/README-developers.md
index 88d08a1724..d5c6096100 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -73,16 +73,31 @@ Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) fil
 
 If you break external projects that are hosted on GitHub, you can use
 the `create_overlays.sh` script to automatically perform most of the
-above steps. In order to do so, call the script as:
-```
-./dev/tools/create_overlays.sh ejgallego 9873 aac_tactics elpi ltac
-```
-replacing `ejgallego` by your GitHub nickname and `9873` by the actual PR
-number. The script will:
+above steps. In order to do so:
 
-- checkout the contributions and prepare the branch/remote so you can
-  just commit the fixes and push,
-- add the corresponding overlay file in `dev/ci/user-overlays`.
+- determine the list of failing projects:
+IDs can be found as ci-XXX1 ci-XXX2 ci-XXX3 in the list of GitLab CI failures;
+- for each project XXXi, look in [ci-basic-overlay.sh](https://github.com/coq/coq/blob/master/dev/ci/ci-basic-overlay.sh)
+to see if the corresponding `XXXi_CI_GITURL` is hosted on GitHub;
+- log on GitHub and fork all the XXXi projects hosted there;
+- call the script as:
+
+    ```
+    ./dev/tools/create_overlays.sh ejgallego 9873 XXX1 XXX2 XXX3
+    ```
+
+    replacing `ejgallego` by your GitHub nickname, `9873` by the actual PR
+number, and selecting the XXXi hosted on GitHub. The script will:
+
+    + checkout the contributions and prepare the branch/remote so you can
+      just commit the fixes and push,
+    + add the corresponding overlay file in `dev/ci/user-overlays`;
+
+- go to `_build_ci/XXXi` to prepare your overlay
+(you can test your modifications by using `make -C ../.. ci-XXXi`)
+and push using `git push ejgallego` (replacing `ejgallego` by your GitHub nickname);
+- finally push the `dev/ci/user-overlays/9873-elgallego-YYY.sh` file on your Coq fork
+(replacing `9873` by the actual PR number, and `ejgallego` by your GitHub nickname).
 
 For problems related to ML-plugins, if you use `dune build` to build
 Coq, it will actually be aware of the broken contributions and perform
@@ -124,7 +139,7 @@ Currently available artifacts are:
 - the Coq documentation, built in the `doc:*` jobs. When submitting a
   documentation PR, this can help reviewers checking the rendered
   result.  **@coqbot** will automatically post links to these
-  artifacts in the PR checks section.  Furthemore, these artifacts are
+  artifacts in the PR checks section.  Furthermore, these artifacts are
   automatically deployed at:
 
   + Coq's Reference Manual [master branch]:
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index f7a8851af7..5f7d0b5789 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -46,9 +46,9 @@
 : "${math_classes_CI_GITURL:=https://github.com/coq-community/math-classes}"
 : "${math_classes_CI_ARCHIVEURL:=${math_classes_CI_GITURL}/archive}"
 
-: "${Corn_CI_REF:=master}"
-: "${Corn_CI_GITURL:=https://github.com/coq-community/corn}"
-: "${Corn_CI_ARCHIVEURL:=${Corn_CI_GITURL}/archive}"
+: "${corn_CI_REF:=master}"
+: "${corn_CI_GITURL:=https://github.com/coq-community/corn}"
+: "${corn_CI_ARCHIVEURL:=${corn_CI_GITURL}/archive}"
 
 ########################################################################
 # Iris
@@ -59,19 +59,19 @@
 : "${stdpp_CI_GITURL:=https://gitlab.mpi-sws.org/iris/stdpp}"
 : "${stdpp_CI_ARCHIVEURL:=${stdpp_CI_GITURL}/-/archive}"
 
-: "${Iris_CI_GITURL:=https://gitlab.mpi-sws.org/iris/iris}"
-: "${Iris_CI_ARCHIVEURL:=${Iris_CI_GITURL}/-/archive}"
+: "${iris_CI_GITURL:=https://gitlab.mpi-sws.org/iris/iris}"
+: "${iris_CI_ARCHIVEURL:=${iris_CI_GITURL}/-/archive}"
 
-: "${lambdaRust_CI_REF:=master}"
-: "${lambdaRust_CI_GITURL:=https://gitlab.mpi-sws.org/iris/lambda-rust}"
-: "${lambdaRust_CI_ARCHIVEURL:=${lambdaRust_CI_GITURL}/-/archive}"
+: "${lambda_rust_CI_REF:=master}"
+: "${lambda_rust_CI_GITURL:=https://gitlab.mpi-sws.org/iris/lambda-rust}"
+: "${lambda_rust_CI_ARCHIVEURL:=${lambda_rust_CI_GITURL}/-/archive}"
 
 ########################################################################
 # HoTT
 ########################################################################
-: "${HoTT_CI_REF:=master}"
-: "${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT}"
-: "${HoTT_CI_ARCHIVEURL:=${HoTT_CI_GITURL}/archive}"
+: "${hott_CI_REF:=master}"
+: "${hott_CI_GITURL:=https://github.com/HoTT/HoTT}"
+: "${hott_CI_ARCHIVEURL:=${hott_CI_GITURL}/archive}"
 
 ########################################################################
 # CoqHammer
@@ -83,16 +83,16 @@
 ########################################################################
 # GeoCoq
 ########################################################################
-: "${GeoCoq_CI_REF:=master}"
-: "${GeoCoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq}"
-: "${GeoCoq_CI_ARCHIVEURL:=${GeoCoq_CI_GITURL}/archive}"
+: "${geocoq_CI_REF:=master}"
+: "${geocoq_CI_GITURL:=https://github.com/GeoCoq/GeoCoq}"
+: "${geocoq_CI_ARCHIVEURL:=${geocoq_CI_GITURL}/archive}"
 
 ########################################################################
 # Flocq
 ########################################################################
-: "${Flocq_CI_REF:=master}"
-: "${Flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq}"
-: "${Flocq_CI_ARCHIVEURL:=${Flocq_CI_GITURL}/-/archive}"
+: "${flocq_CI_REF:=master}"
+: "${flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq}"
+: "${flocq_CI_ARCHIVEURL:=${flocq_CI_GITURL}/-/archive}"
 
 ########################################################################
 # coq-tools
@@ -351,3 +351,10 @@
 : "${metacoq_CI_REF:=master}"
 : "${metacoq_CI_GITURL:=https://github.com/MetaCoq/metacoq}"
 : "${metacoq_CI_ARCHIVEURL:=${metacoq_CI_GITURL}/archive}"
+
+########################################################################
+# SF suite
+########################################################################
+: "${sf_CI_REF:=master}"
+: "${sf_CI_GITURL:=https://github.com/DeepSpec/sf}"
+: "${sf_CI_ARCHIVEURL:=${sf_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-coq-tools.sh b/dev/ci/ci-coq_tools.sh
index 9c95c49c9f..9c95c49c9f 100755
--- a/dev/ci/ci-coq-tools.sh
+++ b/dev/ci/ci-coq_tools.sh
diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh
index a0c714884c..ac3978dc8d 100755
--- a/dev/ci/ci-corn.sh
+++ b/dev/ci/ci-corn.sh
@@ -3,6 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-git_download Corn
+git_download corn
 
-( cd "${CI_BUILD_DIR}/Corn" && ./configure.sh && make && make install )
+( cd "${CI_BUILD_DIR}/corn" && ./configure.sh && make && make install )
diff --git a/dev/ci/ci-cross-crypto.sh b/dev/ci/ci-cross_crypto.sh
index 900d12c1dd..900d12c1dd 100755
--- a/dev/ci/ci-cross-crypto.sh
+++ b/dev/ci/ci-cross_crypto.sh
diff --git a/dev/ci/ci-ext-lib.sh b/dev/ci/ci-ext_lib.sh
index 5eb167d97d..5eb167d97d 100755
--- a/dev/ci/ci-ext-lib.sh
+++ b/dev/ci/ci-ext_lib.sh
diff --git a/dev/ci/ci-fcsl-pcm.sh b/dev/ci/ci-fcsl_pcm.sh
index cb951630c8..cb951630c8 100755
--- a/dev/ci/ci-fcsl-pcm.sh
+++ b/dev/ci/ci-fcsl_pcm.sh
diff --git a/dev/ci/ci-fiat-crypto.sh b/dev/ci/ci-fiat_crypto.sh
index 811fefda35..811fefda35 100755
--- a/dev/ci/ci-fiat-crypto.sh
+++ b/dev/ci/ci-fiat_crypto.sh
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
index 7a9531216e..a3a704091b 100755
--- a/dev/ci/ci-flocq.sh
+++ b/dev/ci/ci-flocq.sh
@@ -3,6 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-git_download Flocq
+git_download flocq
 
-( cd "${CI_BUILD_DIR}/Flocq" && autoconf && ./configure && ./remake "-j${NJOBS}" && ./remake install )
+( cd "${CI_BUILD_DIR}/flocq" && autoconf && ./configure && ./remake "-j${NJOBS}" && ./remake install )
diff --git a/dev/ci/ci-geocoq.sh b/dev/ci/ci-geocoq.sh
index 8c57318477..e4fc983e68 100755
--- a/dev/ci/ci-geocoq.sh
+++ b/dev/ci/ci-geocoq.sh
@@ -5,6 +5,6 @@ ci_dir="$(dirname "$0")"
 
 install_ssralg
 
-git_download GeoCoq
+git_download geocoq
 
-( cd "${CI_BUILD_DIR}/GeoCoq" && ./configure.sh && make )
+( cd "${CI_BUILD_DIR}/geocoq" && ./configure.sh && make )
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index c8e6fe690f..4b92c8cb4d 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -3,6 +3,6 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-git_download HoTT
+git_download hott
 
-( cd "${CI_BUILD_DIR}/HoTT" && ./autogen.sh -skip-submodules && ./configure && make && make validate )
+( cd "${CI_BUILD_DIR}/hott" && ./autogen.sh -skip-submodules && ./configure && make && make validate )
diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-lambda_rust.sh
index d99e140bce..1ef0c2cb8f 100755
--- a/dev/ci/ci-iris-lambda-rust.sh
+++ b/dev/ci/ci-lambda_rust.sh
@@ -5,17 +5,17 @@ ci_dir="$(dirname "$0")"
 
 install_ssreflect
 
-# Setup lambdaRust first
-git_download lambdaRust
+# Setup lambda_rust first
+git_download lambda_rust
 
 # Extract required version of Iris (avoiding "+" which does not work on MacOS :( *)
-Iris_CI_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambdaRust/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
+iris_CI_REF=$(grep -F coq-iris < "${CI_BUILD_DIR}/lambda_rust/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
 
 # Setup Iris
-git_download Iris
+git_download iris
 
 # Extract required version of std++
-stdpp_CI_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/Iris/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
+stdpp_CI_REF=$(grep -F coq-stdpp < "${CI_BUILD_DIR}/iris/opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
 
 # Setup std++
 git_download stdpp
@@ -24,7 +24,7 @@ git_download stdpp
 ( cd "${CI_BUILD_DIR}/stdpp" && make && make install )
 
 # Build and validate Iris
-( cd "${CI_BUILD_DIR}/Iris" && make && make validate && make install )
+( cd "${CI_BUILD_DIR}/iris" && make && make validate && make install )
 
-# Build lambdaRust
-( cd "${CI_BUILD_DIR}/lambdaRust" && make && make install )
+# Build lambda_rust
+( cd "${CI_BUILD_DIR}/lambda_rust" && make && make install )
diff --git a/dev/ci/ci-math-classes.sh b/dev/ci/ci-math_classes.sh
index ae31a8e7f8..ae31a8e7f8 100755
--- a/dev/ci/ci-math-classes.sh
+++ b/dev/ci/ci-math_classes.sh
diff --git a/dev/ci/ci-math-comp.sh b/dev/ci/ci-mathcomp.sh
index cae127ee7b..cae127ee7b 100755
--- a/dev/ci/ci-math-comp.sh
+++ b/dev/ci/ci-mathcomp.sh
diff --git a/dev/ci/ci-sf.sh b/dev/ci/ci-sf.sh
index b9d6215e60..d46e53717f 100755
--- a/dev/ci/ci-sf.sh
+++ b/dev/ci/ci-sf.sh
@@ -3,22 +3,9 @@
 ci_dir="$(dirname "$0")"
 . "${ci_dir}/ci-common.sh"
 
-CIRCLE_SF_TOKEN=00127070c10f5f09574b050e4f08e924764680d2
+git_download sf
 
-# "latest" is disabled due to lack of build credits upstream, thus artifacts fail
-# data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/latest/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -)
-data=$(wget https://circleci.com/api/v1.1/project/gh/DeepSpec/sfdev/1411/artifacts?circle-token=${CIRCLE_SF_TOKEN} -O -)
-
-mkdir -p "${CI_BUILD_DIR}" && cd "${CI_BUILD_DIR}"
-
-sf_lf_CI_TARURL=$(echo "$data"  | jq -rc '.[] | select (.path == "lf.tgz") | .url')
-sf_plf_CI_TARURL=$(echo "$data" | jq -rc '.[] | select (.path == "plf.tgz") | .url')
-sf_vfa_CI_TARURL=$(echo "$data" | jq -rc '.[] | select (.path == "vfa.tgz") | .url')
-
-wget -O - "${sf_lf_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz
-wget -O - "${sf_plf_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz
-wget -O - "${sf_vfa_CI_TARURL}?circle-token=${CIRCLE_SF_TOKEN}" | tar xvz
-
-( cd lf  && make clean && make )
-( cd plf && make clean && make )
-( cd vfa && make clean && make )
+( cd lf-current  && make clean && make )
+( cd plf-current && make clean && make )
+( cd vfa-current && make clean && make )
+# ( cd qc-current && make clean && make )
diff --git a/dev/ci/ci-simple-io.sh b/dev/ci/ci-simple_io.sh
index e7bcd80de7..e7bcd80de7 100755
--- a/dev/ci/ci-simple-io.sh
+++ b/dev/ci/ci-simple_io.sh
diff --git a/dev/ci/ci-verdi-raft.sh b/dev/ci/ci-verdi_raft.sh
index 3bcd52c464..3bcd52c464 100755
--- a/dev/ci/ci-verdi-raft.sh
+++ b/dev/ci/ci-verdi_raft.sh
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index e240ea3ba1..9ee6496ee5 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-03-13-V69"
+# CACHEKEY: "bionic_coq-V2020-05-06-V70"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -39,7 +39,7 @@ ENV COMPILER="4.05.0"
 # with the compiler version.
 ENV BASE_OPAM="num ocamlfind.1.8.1 ounit.2.2.2 odoc.1.5.0" \
     CI_OPAM="menhir.20190626 ocamlgraph.1.8.8" \
-    BASE_ONLY_OPAM="elpi.1.10.2"
+    BASE_ONLY_OPAM="elpi.1.11.0"
 
 # BASE switch; CI_OPAM contains Coq's CI dependencies.
 ENV COQIDE_OPAM="cairo2.0.6.1 lablgtk3-sourceview3.3.1.0"
diff --git a/dev/ci/gitlab.bat b/dev/ci/gitlab.bat
index 3998fc6514..dc6423332f 100755
--- a/dev/ci/gitlab.bat
+++ b/dev/ci/gitlab.bat
@@ -54,7 +54,9 @@ IF "%WINDOWS%" == "enabled_all_addons" (
     -addon=flocq ^
     -addon=interval ^
     -addon=gappa_tool ^
-    -addon=gappa
+    -addon=gappa ^
+    -addon=elpi ^
+    -addon=HB
 ) ELSE (
   SET "EXTRA_ADDONS= "
 )
diff --git a/dev/ci/user-overlays/11922-ppedrot-rm-local-reductionops.sh b/dev/ci/user-overlays/11922-ppedrot-rm-local-reductionops.sh
new file mode 100644
index 0000000000..c9ddb3fb9f
--- /dev/null
+++ b/dev/ci/user-overlays/11922-ppedrot-rm-local-reductionops.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "11922" ] || [ "$CI_BRANCH" = "rm-local-reductionops" ]; then
+
+    equations_CI_REF="rm-local-reductionops"
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+    unicoq_CI_REF="rm-local-reductionops"
+    unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
+
+fi
diff --git a/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh b/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh
new file mode 100644
index 0000000000..b5faabcfe1
--- /dev/null
+++ b/dev/ci/user-overlays/12107-SkySkimmer-no-mod-univs.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12107" ] || [ "$CI_BRANCH" = "no-mod-univs" ]; then
+
+    elpi_CI_REF=no-mod-univs
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh b/dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh
new file mode 100644
index 0000000000..0f8daf418c
--- /dev/null
+++ b/dev/ci/user-overlays/12227-ppedrot-refiner-rm-v82.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12227" ] || [ "$CI_BRANCH" = "refiner-rm-v82" ]; then
+
+    equations_CI_REF="refiner-rm-v82"
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+fi
diff --git a/dev/ci/user-overlays/12267-gares-elpi-1.11.sh b/dev/ci/user-overlays/12267-gares-elpi-1.11.sh
new file mode 100644
index 0000000000..ceb7afe3d1
--- /dev/null
+++ b/dev/ci/user-overlays/12267-gares-elpi-1.11.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12267" ] || [ "$CI_BRANCH" = "elpi-1.11" ]; then
+
+    elpi_CI_REF="coq-master+elpi-1.11"
+    elpi_hb_CI_REF="coq-master+elpi.11"
+
+fi
diff --git a/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh b/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh
new file mode 100644
index 0000000000..50eaf0b109
--- /dev/null
+++ b/dev/ci/user-overlays/8808-herbelin-master+support-binder+term-in-abbrev.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "8808" ] || [ "$CI_BRANCH" = "master+support-binder+term-in-abbrev" ]; then
+
+    elpi_CI_REF=master+adapt-coq8808-syndef-same-expressiveness-notation
+    elpi_CI_GITURL=https://github.com/herbelin/coq-elpi
+
+fi
diff --git a/dev/doc/release-process.md b/dev/doc/release-process.md
index 58c2fcc68a..340b66bbd0 100644
--- a/dev/doc/release-process.md
+++ b/dev/doc/release-process.md
@@ -96,6 +96,8 @@ in time.
 - [ ] Delay non-blocking issues to the appropriate milestone and ensure
   blocking issues are solved. If required to solve some blocking issues,
   it is possible to revert some feature PRs in the version branch only.
+- [ ] Add a new link to the ``'versions'`` list of the refman (in
+      ``html_context`` in ``doc/sphinx/conf.py``).
 
 ## Before the beta release date ##
 
@@ -131,8 +133,12 @@ in time.
   the package managers can Cc `@erikmd` to request that he prepare the necessary configuration for the Docker release in [`coqorg/coq`](https://hub.docker.com/r/coqorg/coq)
   (namely, he'll need to make sure a `coq-bignums` opam package is available in [`extra-dev`](https://github.com/coq/opam-coq-archive/tree/master/extra-dev), respectively [`released`](https://github.com/coq/opam-coq-archive/tree/master/released), so the Docker image gathering `coq` and `coq-bignums` can be built).
 - [ ] Draft a release on GitHub.
-- [ ] Get `@maximedenes` to sign the Windows and MacOS packages and
-  upload them on GitHub.
+- [ ] Sign the Windows and MacOS packages and upload them on GitHub.
+  + The Windows packages must be signed by the Inria IT security service. They
+    should be sent as a link to the binary together with its SHA256 hash in a
+    signed e-mail, via our local contact (currently `@maximedenes`).
+  + The MacOS packages should be signed by our own certificate, by sending them
+    to `@maximedenes`. A detailed step-by-step guide can be found [on the wiki](https://github.com/coq/coq/wiki/SigningReleases).
 - [ ] Prepare a page of news on the website with the link to the GitHub release
   (see [coq/www#63](https://github.com/coq/www/pull/63)).
 - [ ] Upload the new version of the reference manual to the website.