4 files changed, 42 insertions, 1 deletions
diff --git a/dev/ci/ci-iris.sh b/dev/ci/ci-iris.sh
index 9616f3ce00..d29e6f1635 100755
--- a/dev/ci/ci-iris.sh
+++ b/dev/ci/ci-iris.sh
@@ -9,13 +9,15 @@ git_download iris_string_ident
 git_download iris_examples
 
 # Extract required version of Iris (avoiding "+" which does not work on MacOS :( *)
-iris_CI_REF=$(grep -F '"coq-iris"' < "${CI_BUILD_DIR}/iris_examples/coq-iris-examples.opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
+iris_CI_REF=$(grep -F '"coq-iris-heap-lang"' < "${CI_BUILD_DIR}/iris_examples/coq-iris-examples.opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
+[ -n "$iris_CI_REF" ] || { echo "Could not find Iris dependency version" && exit 1; }
 
 # Setup Iris
 git_download iris
 
 # Extract required version of std++
 stdpp_CI_REF=$(grep -F '"coq-stdpp"' < "${CI_BUILD_DIR}/iris/coq-iris.opam" | sed 's/.*"dev\.[0-9][0-9.-]*\.\([0-9a-z][0-9a-z]*\)".*/\1/')
+[ -n "$stdpp_CI_REF" ] || { echo "Could not find stdpp dependency version" && exit 1; }
 
 # Setup std++
 git_download stdpp
diff --git a/dev/ci/user-overlays/12218-proux01-numeral-notations-non-inductive.sh b/dev/ci/user-overlays/12218-proux01-numeral-notations-non-inductive.sh
new file mode 100644
index 0000000000..d9b49ad0d1
--- /dev/null
+++ b/dev/ci/user-overlays/12218-proux01-numeral-notations-non-inductive.sh
@@ -0,0 +1,18 @@
+if [ "$CI_PULL_REQUEST" = "12218" ] || [ "$CI_BRANCH" = "numeral-notations-non-inductive" ]; then
+
+    stdlib2_CI_REF=numeral-notations-non-inductive
+    stdlib2_CI_GITURL=https://github.com/proux01/stdlib2
+
+    hott_CI_REF=numeral-notations-non-inductive
+    hott_CI_GITURL=https://github.com/proux01/HoTT
+
+    paramcoq_CI_REF=numeral-notations-non-inductive
+    paramcoq_CI_GITURL=https://github.com/proux01/paramcoq
+
+    quickchick_CI_REF=numeral-notations-non-inductive
+    quickchick_CI_GITURL=https://github.com/proux01/QuickChick
+
+    metacoq_CI_REF=numeral-notations-non-inductive
+    metacoq_CI_GITURL=https://github.com/proux01/metacoq
+
+fi
diff --git a/dev/ci/user-overlays/13139-ppedrot-clean-hint-constr.sh b/dev/ci/user-overlays/13139-ppedrot-clean-hint-constr.sh
new file mode 100644
index 0000000000..2f70f43a2b
--- /dev/null
+++ b/dev/ci/user-overlays/13139-ppedrot-clean-hint-constr.sh
@@ -0,0 +1,9 @@
+if [ "$CI_PULL_REQUEST" = "13139" ] || [ "$CI_BRANCH" = "clean-hint-constr" ]; then
+
+    equations_CI_REF=clean-hint-constr
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+    fiat_parsers_CI_REF=clean-hint-constr
+    fiat_parsers_CI_GITURL=https://github.com/ppedrot/fiat
+
+fi
diff --git a/dev/doc/critical-bugs b/dev/doc/critical-bugs
index 066facd5db..37619833ac 100644
--- a/dev/doc/critical-bugs
+++ b/dev/doc/critical-bugs
@@ -312,6 +312,18 @@ Conversion machines
   risk: none without using -allow-sprop (off by default in 8.10.0),
         otherwise could be exploited by mistake
 
+Side-effects
+
+  component: side-effects
+  summary: polymorphic side-effects inside monomorphic definitions incorrectly handled as not inlined
+  introduced: ?
+  impacted released versions: at least from 8.6 to 8.12.0
+  impacted coqchk versions: none (no side-effects in the checker)
+  found by: ppedrot
+  exploit: test-suite/bugs/closed/bug_13330.v
+  GH issue number: #13330
+  risk: unlikely to be exploited by mistake, requires the use of unsafe tactics
+
 Conflicts with axioms in library
 
   component: library of real numbers