Sitelet https://github.com/math-comp/math-comp/pull/1616
Skip to content

[CI] Add Coq-Combi - #1616

Open
proux01 wants to merge 1 commit into
math-comp:masterfrom
proux01:ci-coq-combi
Open

proux01 wants to merge 1 commit into
math-comp:masterfrom
proux01:ci-coq-combi

Conversation

@proux01

@proux01 proux01 commented Jun 25, 2026 •

Copy link
Copy Markdown
Contributor

Try adding Coq-Combi to MathComp CI

Overlay (to be merged before the current PR): math-comp/Coq-Combi#18 (merged)

This already enabled to find and fix a bug in mathcomp: #1619

Depends on #1620 (merged)

@proux01
proux01 force-pushed the ci-coq-combi branch 11 times, most recently from 3213d78 to 1ff7ebd Compare June 29, 2026 14:17
@proux01 proux01 added the needs: merge of dependencies PR that depends on another. Documented in the original post of the PR. Review only the increment. label Jun 29, 2026
@proux01 proux01 removed the needs: merge of dependencies PR that depends on another. Documented in the original post of the PR. Review only the increment. label Jun 29, 2026
@proux01
proux01 marked this pull request as ready for review June 30, 2026 06:07
@proux01

proux01 commented Oct 5, 2026

Copy link
Copy Markdown
Contributor Author

@pi8027 the [SubNzRing_isSubComNzRing of {sympoly R[n]} by <:] notation is broken again (c.f. CI) and the deprecation message is not very helpful, how am I expected to instantiate a subNzSemiRingType now?

This branch has not been deployed

No deployments
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.

1 participant