5 files changed, 20 insertions, 2 deletions
diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh
index 6ded97984e..184b90a50b 100755
--- a/dev/ci/ci-hott.sh
+++ b/dev/ci/ci-hott.sh
@@ -7,4 +7,4 @@ HoTT_CI_DIR="${CI_BUILD_DIR}"/HoTT
 
 git_checkout "${HoTT_CI_BRANCH}" "${HoTT_CI_GITURL}" "${HoTT_CI_DIR}"
 
-( cd "${HoTT_CI_DIR}" && ./autogen.sh && ./configure && make )
+( cd "${HoTT_CI_DIR}" && ./autogen.sh && ./configure && make && make validate )
diff --git a/dev/ci/user-overlays/07859-printers.sh b/dev/ci/user-overlays/07859-printers.sh
new file mode 100644
index 0000000000..27f588e214
--- /dev/null
+++ b/dev/ci/user-overlays/07859-printers.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "7859" ] || [ "$CI_BRANCH" = "rm-univ-broken-printing" ]; then
+    Equations_CI_BRANCH=fix-printers
+    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+fi
diff --git a/dev/ci/user-overlays/07908-proj-mind.sh b/dev/ci/user-overlays/07908-proj-mind.sh
new file mode 100644
index 0000000000..293eeb5a5a
--- /dev/null
+++ b/dev/ci/user-overlays/07908-proj-mind.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "7908" ] || [ "$CI_BRANCH" = "proj-mind" ]; then
+    Equations_CI_BRANCH=fix-proj-mind
+    Equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+fi
diff --git a/dev/ci/user-overlays/08063-jasongross-string-eqb.sh b/dev/ci/user-overlays/08063-jasongross-string-eqb.sh
new file mode 100644
index 0000000000..99a11b9fbf
--- /dev/null
+++ b/dev/ci/user-overlays/08063-jasongross-string-eqb.sh
@@ -0,0 +1,6 @@
+#!/bin/sh
+
+if [ "$CI_PULL_REQUEST" = "8063" ] || [ "$CI_BRANCH" = "string-eqb" ]; then
+    quickchick_CI_BRANCH=fix-for-pr-8063
+    quickchick_CI_GITURL=https://github.com/JasonGross/QuickChick
+fi
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index c8385da618..98190b05b5 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -17,7 +17,7 @@ let ppripos (ri,pos) =
   | Reloc_getglobal kn ->
     print_string ("getglob "^(Constant.to_string kn)^"\n")
   | Reloc_proj_name p ->
-    print_string ("proj "^(Constant.to_string p)^"\n")
+    print_string ("proj "^(Projection.Repr.to_string p)^"\n")
   );
    print_flush ()