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.

Sign up for GitHub

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

Jump to bottom

Add coq-mathcomp-classical to Coq Platform #334

Closed
proux01 opened this issue Feb 27, 2023 · 2 comments
Closed

Add coq-mathcomp-classical to Coq Platform #334

proux01 opened this issue Feb 27, 2023 · 2 comments
Assignees
@MSoegtropIMC
Labels
approval: has maintainer agreement kind: package inclusion
Milestone
2023.03

Comments

@proux01
Copy link

proux01 commented Feb 27, 2023

coq-mathcomp-classical is a subpackage of MathComp Analysis since version 0.6.0. This part has been separated as we consider it can be of interest for users that want classical reasoning with mathcomp without requiring the whole Analysis library. Repo and maintainers remain the same as for Analysis.

Cc: @affeldt-aist (following this Zulip discussion https://coq.zulipchat.com/#narrow/stream/237666-math-comp-analysis/topic/new.20package.20mathcomp-classical )
@MSoegtropIMC MSoegtropIMC self-assigned this Apr 6, 2023
@MSoegtropIMC MSoegtropIMC mentioned this issue Apr 6, 2023
Closed
@MSoegtropIMC
Copy link
Collaborator

Note that there is an additional request wit maintainer agreement here: #339.

@MSoegtropIMC MSoegtropIMC added this to the 2023.03 milestone Apr 6, 2023
@MSoegtropIMC
Copy link
Collaborator

The 2023.08 picks for Coq 8.16.1 and 8.17.1 include coq-mathcomp-classical.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@MSoegtropIMC MSoegtropIMC

Labels
approval: has maintainer agreement kind: package inclusion
Projects
None yet
Milestone
2023.03
Development

No branches or pull requests
2 participants
@MSoegtropIMC @proux01