12 files changed, 77 insertions, 22 deletions
diff --git a/dev/base_include b/dev/base_include
index 96a867475d..45e79147c1 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -129,7 +129,7 @@ open Elim
 open Equality
 open Hipattern
 open Inv
-open Leminv
+open Ltac_plugin.Leminv
 open Tacticals
 open Tactics
 open Eqschemes
diff --git a/dev/ci/ci-corn.sh b/dev/ci/ci-corn.sh
index 7d5d70cf90..a0c714884c 100755
--- a/dev/ci/ci-corn.sh
+++ b/dev/ci/ci-corn.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
 
 git_download Corn
 
-( cd "${CI_BUILD_DIR}/Corn" && make && make install )
+( cd "${CI_BUILD_DIR}/Corn" && ./configure.sh && make && make install )
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
index e87483df0a..7a9531216e 100755
--- a/dev/ci/ci-flocq.sh
+++ b/dev/ci/ci-flocq.sh
@@ -5,4 +5,4 @@ ci_dir="$(dirname "$0")"
 
 git_download Flocq
 
-( cd "${CI_BUILD_DIR}/Flocq" && ./autogen.sh && ./configure && ./remake "-j${NJOBS}" )
+( cd "${CI_BUILD_DIR}/Flocq" && autoconf && ./configure && ./remake "-j${NJOBS}" && ./remake install )
diff --git a/dev/ci/docker/bionic_coq/Dockerfile b/dev/ci/docker/bionic_coq/Dockerfile
index 0c8733c75a..e240ea3ba1 100644
--- a/dev/ci/docker/bionic_coq/Dockerfile
+++ b/dev/ci/docker/bionic_coq/Dockerfile
@@ -1,4 +1,4 @@
-# CACHEKEY: "bionic_coq-V2020-03-27-V12"
+# CACHEKEY: "bionic_coq-V2020-03-13-V69"
 # ^^ Update when modifying this file.
 
 FROM ubuntu:bionic
@@ -22,7 +22,7 @@ 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.
-RUN wget https://github.com/ocaml/opam/releases/download/2.0.5/opam-2.0.5-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
+RUN wget https://github.com/ocaml/opam/releases/download/2.0.6/opam-2.0.6-x86_64-linux -O /usr/bin/opam && chmod 755 /usr/bin/opam
 
 # Basic OPAM setup
 ENV NJOBS="2" \
@@ -37,7 +37,7 @@ ENV COMPILER="4.05.0"
 # Common OPAM packages.
 # `num` does not have a version number as the right version to install varies
 # with the compiler version.
-ENV BASE_OPAM="num ocamlfind.1.8.1 dune.2.0.1 ounit.2.2.2 odoc.1.5.0" \
+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"
 
@@ -57,7 +57,7 @@ RUN opam switch create "${COMPILER}+32bit" && eval $(opam env) && \
 
 # EDGE switch
 ENV COMPILER_EDGE="4.10.0" \
-    BASE_OPAM_EDGE="dune-release.1.3.3 ocamlformat.0.13.0"
+    BASE_OPAM_EDGE="dune.2.5.0 dune-release.1.3.3 ocamlformat.0.14.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/11820-SkySkimmer-partial-import.sh b/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh
new file mode 100644
index 0000000000..4170799be7
--- /dev/null
+++ b/dev/ci/user-overlays/11820-SkySkimmer-partial-import.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "11820" ] || [ "$CI_BRANCH" = "partial-import" ]; then
+
+    elpi_CI_REF=partial-import
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+fi
diff --git a/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh b/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh
new file mode 100644
index 0000000000..cd6b408813
--- /dev/null
+++ b/dev/ci/user-overlays/11896-ppedrot-evar-inst-list.sh
@@ -0,0 +1,24 @@
+if [ "$CI_PULL_REQUEST" = "11896" ] || [ "$CI_BRANCH" = "evar-inst-list" ]; then
+
+    coqhammer_CI_REF="evar-inst-list"
+    coqhammer_CI_GITURL=https://github.com/ppedrot/coqhammer
+
+    elpi_CI_REF="evar-inst-list"
+    elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
+
+    equations_CI_REF="evar-inst-list"
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+    metacoq_CI_REF="evar-inst-list"
+    metacoq_CI_GITURL=https://github.com/ppedrot/metacoq
+
+    mtac2_CI_REF="evar-inst-list"
+    mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2
+
+    quickchick_CI_REF="evar-inst-list"
+    quickchick_CI_GITURL=https://github.com/ppedrot/QuickChick
+
+    unicoq_CI_REF="evar-inst-list"
+    unicoq_CI_GITURL=https://github.com/ppedrot/unicoq
+
+fi
diff --git a/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh
new file mode 100644
index 0000000000..6bee3c7bb6
--- /dev/null
+++ b/dev/ci/user-overlays/12023-herbelin-master+fixing-empty-Ltac-v-file.sh
@@ -0,0 +1,15 @@
+if [ "$CI_PULL_REQUEST" = "12023" ] || [ "$CI_BRANCH" = "master+fixing-empty-Ltac-v-file" ]; then
+
+    fiat_crypto_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
+    fiat_crypto_CI_GITURL=https://github.com/herbelin/fiat-crypto
+
+    mtac2_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
+    mtac2_CI_GITURL=https://github.com/herbelin/Mtac2
+
+    metacoq_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
+    metacoq_CI_GITURL=https://github.com/herbelin/template-coq
+
+    unimath_CI_REF=master+pr12023-atomic-tactic-now-qualified-in-ltac-file
+    unimath_CI_GITURL=https://github.com/herbelin/UniMath
+
+fi
diff --git a/dev/doc/build-system.dune.md b/dev/doc/build-system.dune.md
index 0506216541..8b0bf216e3 100644
--- a/dev/doc/build-system.dune.md
+++ b/dev/doc/build-system.dune.md
@@ -18,10 +18,6 @@ Dune will get confused if it finds leftovers of in-tree compilation,
 so please be sure your tree is clean from objects files generated by
 the make-based system.
 
-If you want to build the standard libraries and plugins you should
-call `make -f Makefile.dune voboot`. It is usually enough to do that
-once per-session.
-
 More helper targets are available in `Makefile.dune`, `make -f
 Makefile.dune` will display some help.
 
@@ -55,7 +51,6 @@ Instead, you should use the provided "shims" for running `coqtop` and
 `coqide` in a fast build. In order to use them, do:
 
 ```
-$ make -f Makefile.dune voboot                # Only once per session
 $ dune exec -- dev/shim/coqtop-prelude
 ```
 
@@ -153,7 +148,7 @@ depending on your OCaml version. This is due to several factors:
 
 ## Dropping from coqtop:
 
-After doing `make -f Makefile.dune voboot`, the following commands should work:
+The following commands should work:
 ```
 dune exec -- dev/shim/coqbyte-prelude
 > Drop.
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index eac8d86b0a..9498ab8bbb 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -9,6 +9,13 @@
 
 ### ML API
 
+Proof state and constant declaration:
+
+- A large consolidation of the API handling interactive and
+  non-interactive constant has been performed; low-level APIs are no
+  longer available, and the functionality of the `Proof_global` module
+  has been merged into `Declare`.
+
 Notations:
 
 - Most operators on numerals have moved to file numTok.ml.
@@ -68,7 +75,6 @@ Proof state:
   information related to the constant declaration. Some functions have
   been renamed from `start_proof` to `start_lemma`
 
-
   Plugins that require access to the information about currently
   opened lemmas can add one of the `![proof]` attributes to their
   `mlg` entry, which will refine the type accordingly. See
diff --git a/dev/nixpkgs.nix b/dev/nixpkgs.nix
index b8a696ef21..fb84155392 100644
--- a/dev/nixpkgs.nix
+++ b/dev/nixpkgs.nix
@@ -1,4 +1,4 @@
 import (fetchTarball {
-  url = "https://github.com/NixOS/nixpkgs/archive/34e41a91547e342f6fbc901929134b34000297eb.tar.gz";
-  sha256 = "0mlqxim36xg8aj4r35mpcgqg27wy1dbbim9l1cpjl24hcy96v48w";
+  url = "https://github.com/NixOS/nixpkgs/archive/807ca93fadd5197c2260490de0c76e500562dc05.tar.gz";
+  sha256 = "10yq8bnls77fh3pk5chkkb1sv5lbdgyk1rr2v9xn71rr1k2x563p";
 })
diff --git a/dev/tools/pre-commit b/dev/tools/pre-commit
index 633913aac6..448e224f2e 100755
--- a/dev/tools/pre-commit
+++ b/dev/tools/pre-commit
@@ -16,6 +16,15 @@ then
     1>&2 echo "Warning: ocamlformat is not in path. Cannot check formatting."
 fi
 
+# Verify that the version of ocamlformat matches the one in .ocamlformat
+# The following command will print an error message if that's not the case
+# (and will print nothing if the versions match)
+if ! echo "let () = ()" | "$ocamlformat" --impl - > /dev/null
+then
+    1>&2 echo "Warning: Cannot check formatting."
+    ocamlformat=true
+fi
+
 1>&2 echo "Auto fixing whitespace and formatting issues..."
 
 # We fix whitespace in the index and in the working tree
@@ -43,7 +52,7 @@ if [ -s "$index" ]; then
     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 diff --cached --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true; } 2> /dev/null
     git add -u
     1>&2 echo #newline
 fi
@@ -59,7 +68,7 @@ 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
+    { git diff --name-only -z | grep -E '.*\.mli?$' -z | xargs -0 "$ocamlformat" -i || true; } 2> /dev/null
     1>&2 echo #newline
 fi
 
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 7002cbffac..00050a89e1 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -59,8 +59,8 @@ let prrecarg = function
 let ppwf_paths x = pp (Rtree.pp_tree prrecarg x)
 
 let get_current_context () =
-  try Vernacstate.Proof_global.get_current_context ()
-  with Vernacstate.Proof_global.NoCurrentProof ->
+  try Vernacstate.Declare.get_current_context ()
+  with Vernacstate.Declare.NoCurrentProof ->
     let env = Global.env() in
     Evd.from_env env, env
   [@@ocaml.warning "-3"]
@@ -287,7 +287,7 @@ let constr_display csr =
       "LetIn("^(name_display na)^","^(term_display b)^","
       ^(term_display t)^","^(term_display c)^")"
   | App (c,l) -> "App("^(term_display c)^","^(array_display l)^")\n"
-  | Evar (e,l) -> "Evar("^(Pp.string_of_ppcmds (Evar.print e))^","^(array_display l)^")"
+  | Evar (e,l) -> "Evar("^(Pp.string_of_ppcmds (Evar.print e))^","^(array_display (Array.of_list l))^")"
   | Const (c,u) -> "Const("^(Constant.to_string c)^","^(universes_display u)^")"
   | Ind ((sp,i),u) ->
       "MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^","^(universes_display u)^")"
@@ -383,7 +383,7 @@ let print_pure_constr csr =
       Array.iter (fun x -> print_space (); box_display x) l;
       print_string ")"
   | Evar (e,l) -> print_string "Evar#"; print_int (Evar.repr e); print_string "{";
-      Array.iter (fun x -> print_space (); box_display x) l;
+      List.iter (fun x -> print_space (); box_display x) l;
       print_string"}"
   | Const (c,u) -> print_string "Cons(";
       sp_con_display c;