diff --git a/.github/workflows/coq-proofs.yml b/.github/workflows/coq-proofs.yml
index 8e79e257fb..a172c711c2 100644
--- a/.github/workflows/coq-proofs.yml
+++ b/.github/workflows/coq-proofs.yml
@@ -40,7 +40,23 @@ jobs:
       - name: Install Coq Interval
         run: |
           opam update
-          opam install -y coq-interval.4.9.0
+          # NOT `coq-interval.4.9.0`. That pin is incompatible with the image
+          # this job runs in, and said so as soon as OPAMROOT was fixed and opam
+          # could get far enough to compute a solution:
+          #
+          #     [ERROR] Package conflict!
+          #       * Missing dependency:
+          #         - coq-interval = 4.9.0 -> coq < 8.19~
+          #     No solution found, exiting
+          #
+          # The image is coqorg/coq:8.19. 7 of the 13 proof files `Require Import
+          # Interval.Tactic`, so the dependency is real and cannot be dropped --
+          # only the version can move. Unpinned here deliberately, because the
+          # version that resolves against Coq 8.19 has never been observed in
+          # this job: it has never run this far. The next line records what the
+          # solver chose, and that reading is what a pin should be restored from.
+          opam install -y coq-interval
+          opam list --installed coq-interval
           # Prove the switch is really there before anything depends on it.
           eval $(opam env)
           coqc --version
diff --git a/docs/now/2026-09-06-the-coq-fix-worked-and-uncovered-the-next-defect.md b/docs/now/2026-09-06-the-coq-fix-worked-and-uncovered-the-next-defect.md
new file mode 100644
index 0000000000..3c631245bb
--- /dev/null
+++ b/docs/now/2026-09-06-the-coq-fix-worked-and-uncovered-the-next-defect.md
@@ -0,0 +1,7 @@
+# NOW -- the coq fix worked and uncovered the next defect (2026-09-06)
+
+## the coq fix worked and uncovered the next defect (Refs #3316)
+
+- OPAMROOT fixed the first error: opam now updates and reaches the solver. The job still fails, at a different place, which is what a repair looks like when a workflow has never run far enough to show its second problem.
+- coq-interval 4.9.0 requires coq < 8.19 and the image is coqorg/coq:8.19. 7 of 13 proof files Require Import Interval.Tactic, so the dependency is real; only the pin can move.
+- Unpinned rather than guessed at a version. No version of coq-interval has ever been observed resolving against 8.19 in this job because the job has never got this far. opam list --installed records what the solver picks, and that reading is what a pin should be restored from.