Conversation
| | "rocq-core" {>= "9.0"}) | ||
| "coq-mathcomp-ssreflect" {>= "2.4"} | ||
| "coq-mathcomp-algebra" | ||
| "rocq-core" {>= "9.0"} |
There was a problem hiding this comment.
Apparently, the Rocq-community templates don't let us replace coq with rocq-core here yet.
| "coq-mathcomp-bigenough" | ||
| "coq-mathcomp-finmap" |
There was a problem hiding this comment.
I guess this should be
| "coq-mathcomp-bigenough" | |
| "coq-mathcomp-finmap" | |
| "rocq-mathcomp-bigenough" | |
| "rocq-mathcomp-finmap" |
There was a problem hiding this comment.
I performed this change, and it breaks finmap in CI.
There was a problem hiding this comment.
Ok, I guess the thing is that only coq-mathcomp-finmap has the dev version. This should be fixed in the opam repo.
There was a problem hiding this comment.
And bigenough has the same issue.
|
@proux01 To answer your comment (#123 (comment)), we need to patch two lines in the new opam file ( |
2 participants
#123 (comment)
Also, I think it's the right time to start requiring Rocq 9.0. It allows us to refactor the proof scripts, but I will do it later.