2 files changed, 26 insertions, 2 deletions
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/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;