Skip to content

Commit 8fc7d12

Browse files
authored
Merge pull request #3853 from proux01/mathcomp-reals-stdlib
rocq-mathcomp-reals-stdlib: fix Stdlib dep
2 parents 0bfb6f8 + 0b552c2 commit 8fc7d12

1 file changed

Lines changed: 1 addition & 2 deletions

File tree

  • released/packages/rocq-mathcomp-reals-stdlib/rocq-mathcomp-reals-stdlib.1.18.0

released/packages/rocq-mathcomp-reals-stdlib/rocq-mathcomp-reals-stdlib.1.18.0/opam

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -14,8 +14,7 @@ the Coq proof-assistant using the Mathematical Components library and Stdlib."""
1414
build: [make "-C" "reals_stdlib" "-j%{jobs}%"]
1515
install: [make "-C" "reals_stdlib" "install"]
1616
depends: [
17-
("coq" {< "8.21~"}
18-
| "rocq-stdlib" { (>= "9.0" & < "9.1~") | (= "dev") })
17+
"rocq-stdlib"
1918
"rocq-mathcomp-reals" { = version}
2019
]
2120

0 commit comments

Comments
 (0)