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

bigenough dependency for mathcomp-analysis and mathcomp-finmap #1124

Open
palmskog opened this issue Jan 31, 2020 · 0 comments
Open

bigenough dependency for mathcomp-analysis and mathcomp-finmap #1124

palmskog opened this issue Jan 31, 2020 · 0 comments

Comments

@palmskog
Copy link
Contributor

palmskog commented Jan 31, 2020

It looks like the package coq-mathcomp-finmap introduced the following dependency for version 1.2.0:

"coq-mathcomp-bigenough" { (>= "1.0.0" & < "1.1.0~") }

However, as far as I can see, this dependency is not used by coq-mathcomp-finmap itself, in all versions up to and including the most recent one, 1.4.0.

Nevertheless, the package coq-mathcomp-analysis depends on coq-mathcomp-finmap and on coq-mathcomp-bigenough - but only the former dependency is explicitly listed in, e.g., coq-mathcomp-analysis.0.2.3.

It's probably a good idea to refactor the various OPAM package versions to reflect these dependency relationships.

cc: @anton-trunov @CohenCyril

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

No branches or pull requests

1 participant