9 files changed, 32 insertions, 5 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 628e892910..784da6f971 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -70,7 +70,7 @@
 # Flocq
 ########################################################################
 : "${Flocq_CI_BRANCH:=master}"
-: "${Flocq_CI_GITURL:=https://scm.gforge.inria.fr/anonscm/git/flocq/flocq.git}"
+: "${Flocq_CI_GITURL:=https://gitlab.inria.fr/flocq/flocq.git}"
 
 ########################################################################
 # Coquelicot
diff --git a/dev/ci/ci-common.sh b/dev/ci/ci-common.sh
index 1838db5d01..05fa33e972 100644
--- a/dev/ci/ci-common.sh
+++ b/dev/ci/ci-common.sh
@@ -2,6 +2,10 @@
 
 set -xe
 
+# default value for NJOBS
+: "${NJOBS:=1}"
+export NJOBS
+
 if [ -n "${GITLAB_CI}" ];
 then
     export COQBIN="$PWD/_install_ci/bin"
diff --git a/dev/ci/ci-compcert.sh b/dev/ci/ci-compcert.sh
index fc3cef3426..6a0ce2aefa 100755
--- a/dev/ci/ci-compcert.sh
+++ b/dev/ci/ci-compcert.sh
@@ -5,7 +5,7 @@ source ${ci_dir}/ci-common.sh
 
 CompCert_CI_DIR=${CI_BUILD_DIR}/CompCert
 
-opam install -j ${NJOBS} -y menhir
+opam install -j "$NJOBS" -y menhir
 git_checkout ${CompCert_CI_BRANCH} ${CompCert_CI_GITURL} ${CompCert_CI_DIR}
 
 ( cd ${CompCert_CI_DIR} && ./configure -ignore-coq-version x86_32-linux && make && make check-proof )
diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh
index cf24d202d9..267e13359b 100755
--- a/dev/ci/ci-iris-lambda-rust.sh
+++ b/dev/ci/ci-iris-lambda-rust.sh
@@ -34,8 +34,8 @@ git_checkout ${stdpp_CI_BRANCH} ${stdpp_URL_PARTS[0]} ${stdpp_CI_DIR} ${stdpp_UR
 # Build std++
 ( cd ${stdpp_CI_DIR} && make && make install )
 
-# Build iris
-( cd ${Iris_CI_DIR} && make && make install )
+# Build and validate (except on Travis, i.e., skip if TRAVIS is non-empty) Iris
+( cd ${Iris_CI_DIR} && make && (test -n "${TRAVIS}" || make validate) && make install )
 
 # Build lambdaRust
 ( cd ${lambdaRust_CI_DIR} && make && make install )
diff --git a/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh b/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh
new file mode 100644
index 0000000000..8a50fb1111
--- /dev/null
+++ b/dev/ci/user-overlays/06535-fix-push-rel-to-named.sh
@@ -0,0 +1,4 @@
+if [ "$CI_PULL_REQUEST" = "6535" ] || [ "$CI_BRANCH" = "fix-push-rel-to-named" ]; then
+    Equations_CI_BRANCH=fix-6535
+    Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+fi
diff --git a/dev/ci/user-overlays/06686-ccnv-no-proj.sh b/dev/ci/user-overlays/06686-ccnv-no-proj.sh
new file mode 100644
index 0000000000..3a3ab44e03
--- /dev/null
+++ b/dev/ci/user-overlays/06686-ccnv-no-proj.sh
@@ -0,0 +1,4 @@
+if [ "$CI_PULL_REQUEST" = "6686" ] || [ "$CI_BRANCH" = "ccnv-no-proj" ]; then
+    Equations_CI_BRANCH=ccnv-fixes
+    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index e616bd5663..aef62b0092 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -58,6 +58,17 @@ Declaration of printers for arguments used only in vernac command
   happen. An alternative is to register the corresponding argument as
   a value, using "Geninterp.register_val0 wit None".
 
+### STM API
+
+The STM API has seen a general overhaul. The main change is the
+introduction of a "Coq document" type, which all operations now take
+as a parameter. This effectively functionalize the STM API and will
+allow in the future to handle several documents simultaneously.
+
+The main remarkable point is that key implicit global parameters such
+as load-paths and required modules are now arguments to the document
+creation function. This helps enforcing some key invariants.
+
 ### XML IDE Protocol
 
 - Before 8.8, `Query` only executed the first command present in the
diff --git a/dev/tools/sudo-apt-get-update.sh b/dev/tools/sudo-apt-get-update.sh
new file mode 100755
index 0000000000..f8bf6bed41
--- /dev/null
+++ b/dev/tools/sudo-apt-get-update.sh
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+
+(sudo apt-get update "$@" 2>&1 || echo 'E: update failed') | tee /tmp/apt.err
+! grep -q '^\(E:\|W: Failed to fetch\)' /tmp/apt.err || exit $?
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index 8e43bf6ed0..f819d2e6a9 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -3,7 +3,7 @@ open Term
 open Names
 open Cbytecodes
 open Cemitcodes
-open Vm
+open Vmvalues
 
 let ppripos (ri,pos) =
   (match ri with