From 885f2e6caaf9b1dd78e6e1679fbcfc3bafbfb738 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 28 Jul 2026 04:45:25 +0000 Subject: [PATCH] Add missing analysis dependency to experimental reals --- .../coq-mathcomp-experimental-reals.dev/opam | 1 + 1 file changed, 1 insertion(+) diff --git a/extra-dev/packages/coq-mathcomp-experimental-reals/coq-mathcomp-experimental-reals.dev/opam b/extra-dev/packages/coq-mathcomp-experimental-reals/coq-mathcomp-experimental-reals.dev/opam index 64d137dcc5..868b3e7e71 100644 --- a/extra-dev/packages/coq-mathcomp-experimental-reals/coq-mathcomp-experimental-reals.dev/opam +++ b/extra-dev/packages/coq-mathcomp-experimental-reals/coq-mathcomp-experimental-reals.dev/opam @@ -17,6 +17,7 @@ Beware that this still contains a few Admitted.""" build: [make "-C" "experimental_reals" "-j%{jobs}%"] install: [make "-C" "experimental_reals" "install"] depends: [ + "coq-mathcomp-analysis" { = version} "coq-mathcomp-reals" { = version} "coq-mathcomp-bigenough" { (>= "1.0.0") } ]