9 files changed, 52 insertions, 13 deletions
diff --git a/dev/ci/azure-opam.sh b/dev/ci/azure-opam.sh
index ee6c62673b..7b3e2703b8 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.0+mingw64c
+OPAM_VARIANT=ocaml-variants.4.09.1+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-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index bd7ee46358..70e3fe5c69 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -330,3 +330,10 @@
 : "${perennial_CI_REF:=master}"
 : "${perennial_CI_GITURL:=https://github.com/mit-pdos/perennial}"
 : "${perennial_CI_ARCHIVEURL:=${perennial_CI_GITURL}/archive}"
+
+########################################################################
+# metacoq
+########################################################################
+: "${metacoq_CI_REF:=master}"
+: "${metacoq_CI_GITURL:=https://github.com/MetaCoq/metacoq}"
+: "${metacoq_CI_ARCHIVEURL:=${metacoq_CI_GITURL}/archive}"
diff --git a/dev/ci/ci-equations.sh b/dev/ci/ci-equations.sh
index 871d033f5b..30047e624b 100755
--- a/dev/ci/ci-equations.sh
+++ b/dev/ci/ci-equations.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
 
 git_download equations
 
-( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci)
+( cd "${CI_BUILD_DIR}/equations" && ./configure.sh coq && make ci && make install )
diff --git a/dev/ci/ci-metacoq.sh b/dev/ci/ci-metacoq.sh
new file mode 100755
index 0000000000..1302065961
--- /dev/null
+++ b/dev/ci/ci-metacoq.sh
@@ -0,0 +1,8 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download metacoq
+
+( cd "${CI_BUILD_DIR}/metacoq" && ./configure.sh local && make ci-local && make install )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 979b5917d4..e56e4d38ea 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2019-03-14-V14"
+# CACHEKEY: "bionic_coq-V2020-03-19-V29"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -18,7 +18,7 @@ RUN apt-get update -qq && apt-get install --no-install-recommends -y -qq \
         texlive-science tipa
 
 # More dependencies of the sphinx doc
-RUN pip3 install sphinx==1.7.8 sphinx_rtd_theme==0.2.5b2 \
+RUN pip3 install sphinx==1.8.0 sphinx_rtd_theme==0.2.5b2 \
                  antlr4-python3-runtime==4.7.1 sphinxcontrib-bibtex==0.4.0
 
 # We need to install OPAM 2.0 manually for now.
@@ -56,8 +56,8 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
     opam install $BASE_OPAM
 
 # EDGE switch
-ENV COMPILER_EDGE="4.09.0" \
-    BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.12"
+ENV COMPILER_EDGE="4.09.1" \
+    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
 # `ci-template-flambda` with everything.
diff --git a/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh b/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh
new file mode 100644
index 0000000000..6928925e54
--- /dev/null
+++ b/dev/ci/user-overlays/11731-ejgallego-proof+more_naming_unif.sh
@@ -0,0 +1,12 @@
+if [ "$CI_PULL_REQUEST" = "11731" ] || [ "$CI_BRANCH" = "proof+more_naming_unif" ]; then
+
+    equations_CI_REF=proof+more_naming_unif
+    equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
+
+    rewriter_CI_REF=proof+more_naming_unif
+    rewriter_CI_GITURL=https://github.com/ejgallego/rewriter
+
+    elpi_CI_REF=proof+more_naming_unif
+    elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi
+
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index d5938713d6..b82388675c 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,13 +1,20 @@
 ## Changes between Coq 8.11 and Coq 8.12
 
-### ML API
+### Code formatting
 
-Types `precedence`, `parenRelation`, `tolerability` in
-`notgram_ops.ml` have been reworked. See `entry_level` and
-`entry_relative_level` in `constrexpr.ml`.
+- The automatic code formatting tool `ocamlformat` is enabled now for
+  the micromega codebase. Version 0.13.0 is required. See
+  `ocalmformat`'s documentation for more details on integration with
+  your editor.
 
 ### ML API
 
+Notations:
+
+- Types `precedence`, `parenRelation`, `tolerability` in
+  `notgram_ops.ml` have been reworked. See `entry_level` and
+  `entry_relative_level` in `constrexpr.ml`.
+
 Exception handling:
 
 - Coq's custom `Backtrace` module has been removed in favor of OCaml's
@@ -21,6 +28,11 @@ Exception handling:
   + printers are of type `exn -> Pp.t option` [`None` == not handled]
   + it is forbidden for exception printers to raise.
 
+- Refiner.catchable_exception is deprecated, use instead
+  CErrors.noncritical in try-with block. Note that nothing is needed in
+  tclORELSE block since the exceptions there are supposed to be
+  non-critical by construction.
+
 Printers:
 
 - Functions such as Printer.pr_lconstr_goal_style_env have been
diff --git a/dev/dune-workspace.all b/dev/dune-workspace.all
index 49e338d0a5..556493ffad 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.0)))
-(context (opam (switch 4.09.0+flambda)))
+(context (opam (switch 4.09.1)))
+(context (opam (switch 4.09.1+flambda)))
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index ebe704b88a..96dbf9142b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -82,7 +82,7 @@ let ppsconstr x = ppconstr (Mod_subst.force_constr x)
 let ppconstr_univ x = Constrextern.with_universes ppconstr x
 let ppglob_constr = (fun x -> pp(pr_lglob_constr_env (Global.env()) x))
 let pppattern = (fun x -> pp(envpp pr_constr_pattern_env x))
-let pptype = (fun x -> try pp(envpp pr_ltype_env x) with e -> pp (str (Printexc.to_string e)))
+let pptype = (fun x -> try pp(envpp (fun env evm t -> pr_ltype_env env evm t) x) with e -> pp (str (Printexc.to_string e)))
 let ppfconstr c = ppconstr (CClosure.term_of_fconstr c)
 
 let ppbigint n = pp (str (Bigint.to_string n));;