Prosa does not compile with Coq 8.15.0 and mathcomp 1.14.0
There are some Ltac errors. See CI job #169764.
Designs
No child items are currently assigned. Use child items to break down this issue into smaller parts.
Related merge requests 1
When this merge request is accepted, this issue will be closed automatically.
Activity
It seems the
exploittactic needs to be updated.@sbozhko: Sergey, can you please take care of this in the branch
coq-version-bump?mentioned in merge request !184 (merged)
closed with merge request !184 (merged)
Please register or sign in to reply