Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

coq-fcsl-pcm.2.0.0 doesn't support coq-hierarchy-builder.1.8.0 #3272

Merged
merged 2 commits into from
Dec 22, 2024

Conversation

palmskog
Copy link
Collaborator

Here is the error:

File "./pcm/pcm.v", line 429, characters 0-76:
Error:
HB: choice.hasChoice.axioms_ is not a factory or its library (mathcomp.ssreflect.choice) was not correctly imported

@aleksnanevski it's a good idea to record the dependency on HB in the meta/opam file in the fcsl-pcm repo.

@aleksnanevski
Copy link
Contributor

Hi. The dev version of coq-fcsl-pcm (the master branch) actually works with the new hb. How to make that dependency explicit in meta/opam?

Copy link
Contributor

@aleksnanevski aleksnanevski left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ok. i guess it's time for a new release.

@palmskog palmskog merged commit 593a060 into coq:master Dec 22, 2024
3 checks passed
@palmskog palmskog deleted the pcm-hb-1.8 branch December 22, 2024 18:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants