6 files changed, 25 insertions, 16 deletions
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 48e01e9e93..2adc7d8dcc 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -142,7 +142,7 @@
 ########################################################################
 # Equations
 ########################################################################
-: "${Equations_CI_BRANCH:=8.8+alpha}"
+: "${Equations_CI_BRANCH:=master}"
 : "${Equations_CI_GITURL:=https://github.com/mattam82/Coq-Equations.git}"
 
 ########################################################################
diff --git a/dev/ci/ci-iris-lambda-rust.sh b/dev/ci/ci-iris-lambda-rust.sh
index b019fa059a..1af0f634c4 100755
--- a/dev/ci/ci-iris-lambda-rust.sh
+++ b/dev/ci/ci-iris-lambda-rust.sh
@@ -9,27 +9,20 @@ lambdaRust_CI_DIR="${CI_BUILD_DIR}/lambdaRust"
 
 install_ssreflect
 
-# Add or update the opam repo we need for dependency resolution
-opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git -p 0 || opam update iris-dev
-
 # Setup lambdaRust first
 git_checkout "${lambdaRust_CI_BRANCH}" "${lambdaRust_CI_GITURL}" "${lambdaRust_CI_DIR}"
 
 # Extract required version of Iris
-Iris_VERSION=$(grep -F coq-iris < "${lambdaRust_CI_DIR}/opam" | grep -E 'dev\.([0-9.-]+)' -o)
-Iris_URL=$(opam show "coq-iris.$Iris_VERSION" -f upstream-url)
-read -r -a Iris_URL_PARTS <<< "$(echo "$Iris_URL" | tr '#' ' ')"
+Iris_SHA=$(grep -F coq-iris < "${lambdaRust_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/')
 
 # Setup Iris
-git_checkout "${Iris_CI_BRANCH}" "${Iris_URL_PARTS[0]}" "${Iris_CI_DIR}" "${Iris_URL_PARTS[1]}"
+git_checkout "${Iris_CI_BRANCH}" "${Iris_CI_GITURL}" "${Iris_CI_DIR}" "${Iris_SHA}"
 
 # Extract required version of std++
-stdpp_VERSION=$(grep -F coq-stdpp < "${Iris_CI_DIR}/opam" | grep -E 'dev\.([0-9.-]+)' -o)
-stdpp_URL=$(opam show "coq-stdpp.$stdpp_VERSION" -f upstream-url)
-read -r -a stdpp_URL_PARTS <<< "$(echo "$stdpp_URL" | tr '#' ' ')"
+stdpp_SHA=$(grep -F coq-stdpp < "${Iris_CI_DIR}/opam" | sed 's/.*"dev\.[0-9.-]\+\.\([0-9a-z]\+\)".*/\1/')
 
 # Setup std++
-git_checkout "${stdpp_CI_BRANCH}" "${stdpp_URL_PARTS[0]}" "${stdpp_CI_DIR}" "${stdpp_URL_PARTS[1]}"
+git_checkout "${stdpp_CI_BRANCH}" "${stdpp_CI_GITURL}" "${stdpp_CI_DIR}" "${stdpp_SHA}"
 
 # Build std++
 ( cd "${stdpp_CI_DIR}" && make && make install )
diff --git a/dev/ci/user-overlays/07136-evar-map-econstr.sh b/dev/ci/user-overlays/07136-evar-map-econstr.sh
new file mode 100644
index 0000000000..06aa62726d
--- /dev/null
+++ b/dev/ci/user-overlays/07136-evar-map-econstr.sh
@@ -0,0 +1,7 @@
+if [ "$CI_PULL_REQUEST" = "7136" ] || [ "$CI_BRANCH" = "evar-map-econstr" ]; then
+    Equations_CI_BRANCH=8.9+alpha
+    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations.git
+
+    Elpi_CI_BRANCH=coq-7136
+    Elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi.git
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index ab78b0956f..1a24f23e5a 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,3 +1,12 @@
+## Changes between Coq 8.8 and Coq 8.9
+
+### ML API
+
+Proof engine
+
+  More functions have been changed to use `EConstr`, notably the
+  functions in `Evd`.
+
 ## Changes between Coq 8.7 and Coq 8.8
 
 ### Bug tracker
diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit
index a514b8866a..b56925c370 100755
--- a/dev/tools/pre-commit
+++ b/dev/tools/pre-commit
@@ -27,8 +27,8 @@ then
 
     # reset work tree and index
     # NB: untracked files which were not added are untouched
-    git apply --cached -R "$index"
-    git apply -R "$tree"
+    git apply --whitespace=nowarn --cached -R "$index"
+    git apply --whitespace=nowarn -R "$tree"
 
     # Fix index
     # For end of file newlines we must go through the worktree
@@ -45,7 +45,7 @@ then
     # making git fail. Don't fail now: we fix the worktree first.
     if [ -s "$fixed_index" ]
     then
-        git apply -R "$fixed_index"
+        git apply --whitespace=nowarn -R "$fixed_index"
     fi
 
     # Fix worktree
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index ba0c54407c..f9b4025866 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -181,7 +181,7 @@ let ppproofview p =
   pp(pr_enum Goal.pr_goal gls ++ fnl () ++ Termops.pr_evar_map (Some 1) sigma)
 
 let ppopenconstr (x : Evd.open_constr) =
-  let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ envpp pr_constr_env c)
+  let (evd,c) = x in pp (Termops.pr_evar_map (Some 2) evd ++ envpp pr_econstr_env c)
 (* spiwack: deactivated until a replacement is found
 let pppftreestate p = pp(print_pftreestate p)
 *)