Skip to content

Conversation

andres-erbsen
Copy link
Contributor

This change adapts math-classes for a future stdlib PR removing Zmod.

The current definition of Zmod in stdlib is as follows:

#[deprecated(since="8.17",note="Use Coq.ZArith.BinIntDef.Z.modulo instead")]
Notation Zmod := Z.modulo (only parsing).

I am looking to remove that definition shortly, and to reuse the name for something incompatible.

Thanks!

@andres-erbsen
Copy link
Contributor Author

The CI failure appears unrelated:

  Error response from daemon: No such image: coqorg/coq:dev
  Error response from daemon: manifest for coqorg/coq:dev not found: manifest unknown: manifest unknown

@spitters
Copy link
Collaborator

spitters commented May 9, 2025

Thanks!

Could the CI issue be due to the name change? I guess it's something that shows up on many places on the platform.
@Zimmi48 may know more. I couldn't find the github handle of Sylvain Borgogno...

@SkySkimmer
Copy link
Contributor

Fix ci #135

@spitters
Copy link
Collaborator

spitters commented May 9, 2025

Thanks @SkySkimmer ! I've restarted the CI.

@SkySkimmer SkySkimmer closed this May 9, 2025
@SkySkimmer SkySkimmer reopened this May 9, 2025
@spitters spitters merged commit a2920bf into rocq-community:master May 9, 2025
7 of 9 checks passed
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.

3 participants