6 files changed, 43 insertions, 29 deletions
diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh
index 7b3e2703b8..64936cd236 100755
--- a/dev/ci/azure-opam.sh
+++ b/dev/ci/azure-opam.sh
@@ -2,7 +2,7 @@
 
 set -e -x
 
-OPAM_VARIANT=ocaml-variants.4.09.1+mingw64c
+OPAM_VARIANT=ocaml-variants.4.10.0+mingw64c
 
 wget https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz -O opam64.tar.xz
 tar -xf opam64.tar.xz
diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh
index 756f54dfbd..a21310cbd5 100755
--- a/dev/ci/ci-bignums.sh
+++ b/dev/ci/ci-bignums.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
 
 git_download bignums
 
-( cd "${CI_BUILD_DIR}/bignums" && make && make install)
+( cd "${CI_BUILD_DIR}/bignums" && make && make install && cd tests && make)
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index e56e4d38ea..0c8733c75a 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-03-19-V29"
+# CACHEKEY: "bionic_coq-V2020-03-27-V12"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -56,7 +56,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
     opam install $BASE_OPAM
 
 # EDGE switch
-ENV COMPILER_EDGE="4.09.1" \
+ENV COMPILER_EDGE="4.10.0" \
     BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.13.0"
 
 # EDGE+flambda switch, we install CI_OPAM as to be able to use
diff --git a/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh
new file mode 100644
index 0000000000..e3a8eb07f3
--- /dev/null
+++ b/dev/ci/user-overlays/11818-ejgallego-proof+remove_special_case_first_declaration_in_mutual.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "11818" ] || [ "$CI_BRANCH" = "proof+remove_special_case_first_declaration_in_mutual" ]; then
+
+    metacoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+    metacoq_CI_GITURL=https://github.com/ejgallego/metacoq
+
+    elpi_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+    paramcoq_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+    paramcoq_CI_GITURL=https://github.com/ejgallego/paramcoq
+
+    equations_CI_REF=proof+remove_special_case_first_declaration_in_mutual
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+fi
diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all
index 556493ffad..d6348a3624 100644
--- a/dev/dune-workspace.all
+++ b/dev/dune-workspace.all
@@ -3,5 +3,5 @@
 ; Add custom flags here. Default developer profile is `dev`
 (context (opam (switch 4.05.0)))
 (context (opam (switch 4.05.0+32bit)))
-(context (opam (switch 4.09.1)))
-(context (opam (switch 4.09.1+flambda)))
+(context (opam (switch 4.10.0)))
+(context (opam (switch 4.10.0+flambda)))
diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit
index 9620e7bc8c..633913aac6 100755
--- a/dev/tools/pre-commit
+++ b/dev/tools/pre-commit
@@ -33,44 +33,43 @@ git diff-index -p HEAD > "$tree"
 
 # reset work tree and index
 # NB: untracked files which were not added are untouched
-git apply --whitespace=nowarn --cached -R "$index"
-git apply --whitespace=nowarn -R "$tree"
+if [ -s "$index" ]; then git apply --whitespace=nowarn --cached -R "$index"; fi
+if [ -s "$tree" ]; then git apply --whitespace=nowarn -R "$tree"; fi
 
 # Fix index
 # For end of file newlines we must go through the worktree
-1>&2 echo "Fixing staged changes..."
-git apply --cached --whitespace=fix "$index"
-git apply --whitespace=fix "$index" 2>/dev/null # no need to repeat yourself
-git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix
-git diff --cached --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true
-git add -u
-1>&2 echo #newline
+if [ -s "$index" ]; then
+    1>&2 echo "Fixing staged changes..."
+    git apply --cached --whitespace=fix "$index"
+    git apply --whitespace=fix "$index" 2>/dev/null # no need to repeat yourself
+    git diff --cached --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix
+    git diff --cached --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true
+    git add -u
+    1>&2 echo #newline
+fi
 
 # reset work tree
 git diff-index -p --cached HEAD > "$fixed_index"
 # If all changes were bad whitespace changes the patch is empty
 # making git fail. Don't fail now: we fix the worktree first.
-if [ -s "$fixed_index" ]
-then
-    git apply --whitespace=nowarn -R "$fixed_index"
-fi
+if [ -s "$fixed_index" ]; then git apply --whitespace=nowarn -R "$fixed_index"; fi
 
 # Fix worktree
-1>&2 echo "Fixing unstaged changes..."
-git apply --whitespace=fix "$tree"
-git diff --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix
-git diff --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true
-1>&2 echo #newline
+if [ -s "$tree" ]; then
+    1>&2 echo "Fixing unstaged changes..."
+    git apply --whitespace=fix "$tree"
+    git diff --name-only -z | xargs -0 dev/tools/check-eof-newline.sh --fix
+    git diff --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true
+    1>&2 echo #newline
+fi
 
-if ! [ -s "$fixed_index" ]
-then
-    1>&2 echo "No changes after fixing whitespace and formatting issues!"
+if [ -s "$index" ] && ! [ -s "$fixed_index" ]; then
+    1>&2 echo "Fixing whitespace and formatting issues cancelled all changes."
     exit 1
 fi
 
 # Check that we did fix whitespace
-if ! git diff-index --check --cached HEAD;
-then
+if ! git diff-index --check --cached HEAD; then
     1>&2 echo "Auto-fixing whitespace failed: errors remain."
     1>&2 echo "This may fix itself if you try again."
     1>&2 echo "(Consider whether the number of errors decreases after each run.)"