8 files changed, 61 insertions, 6 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/README-developers.md b/dev/ci/README-developers.md
index 6a740b9033..88d08a1724 100644
--- a/dev/ci/README-developers.md
+++ b/dev/ci/README-developers.md
@@ -72,10 +72,10 @@ Moreover your PR must absolutely update the [`CHANGES.md`](../../CHANGES.md) fil
 ### Experimental automatic overlay creation and building
 
 If you break external projects that are hosted on GitHub, you can use
-the `create-overlays.sh` script to automatically perform most of the
+the `create_overlays.sh` script to automatically perform most of the
 above steps. In order to do so, call the script as:
 ```
-./dev/tools/create-overlays.sh ejgallego 9873 aac_tactics elpi ltac
+./dev/tools/create_overlays.sh ejgallego 9873 aac_tactics elpi ltac
 ```
 replacing `ejgallego` by your GitHub nickname and `9873` by the actual PR
 number. The script will:
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index c18e556da8..88f410ef04 100755
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -95,6 +95,13 @@
 : "${Flocq_CI_ARCHIVEURL:=${Flocq_CI_GITURL}/-/archive}"
 
 ########################################################################
+# coq-tools
+########################################################################
+: "${coq_tools_CI_REF:=master}"
+: "${coq_tools_CI_GITURL:=https://github.com/JasonGross/coq-tools}"
+: "${coq_tools_CI_ARCHIVEURL:=${coq_tools_CI_GITURL}/archive}"
+
+########################################################################
 # Coquelicot
 ########################################################################
 : "${coquelicot_CI_REF:=master}"
diff --git a/dev/ci/ci-coq-tools.sh b/dev/ci/ci-coq-tools.sh
new file mode 100755
index 0000000000..9c95c49c9f
--- /dev/null
+++ b/dev/ci/ci-coq-tools.sh
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+
+ci_dir="$(dirname "$0")"
+. "${ci_dir}/ci-common.sh"
+
+git_download coq_tools
+
+( cd "${CI_BUILD_DIR}/coq_tools" && make check || \
+  { RV=$?; echo "The build broke, if an overlay is needed, mention @JasonGross in describing the expected change in Coq that needs to be taken into account, and he'll prepare a fix for coq-tools"; exit $RV; } )
diff --git a/dev/ci/ci-flocq.sh b/dev/ci/ci-flocq.sh
index e9f8324f28..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" && autoconf && ./configure && ./remake "-j${NJOBS}" )
+( cd "${CI_BUILD_DIR}/Flocq" && autoconf && ./configure && ./remake "-j${NJOBS}" && ./remake install )
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/top_printers.ml b/dev/top_printers.ml
index 542893ad0b..00050a89e1 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -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;