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

deprecate Cyclic.ZModulo.ZModulo #16914

Merged
merged 2 commits into from Dec 9, 2022
Merged

deprecate Cyclic.ZModulo.ZModulo #16914

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
8275ecd
deprecate Cyclic.ZModulo.ZModulo
andres-erbsen Nov 25, 2022
0e81577
add changelog entry
andres-erbsen Nov 25, 2022
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
7 changes: 7 additions & 0 deletions doc/changelog/11-standard-library/16914-deprecate-ZModulo.rst
View file
Open in desktop
@@ -0,0 +1,7 @@
- **Deprecated:** :g:`Cyclic.ZModulo.ZModulo` because there have been no known
use cases for this module and because it does not implement `Z/nZ` for
arbitrary `n` as one might expect based on the name. The same construction
will remain a part of the Coq test suite to ensure consistency of
`CyclicAxioms`
(`#16914 <https://github.com/coq/coq/pull/16914>`_,
by Andres Erbsen).
2 changes: 2 additions & 0 deletions theories/Numbers/Cyclic/ZModulo/ZModulo.v
View file
Open in desktop
Expand Up @@ -11,6 +11,8 @@
(** * Type [Z] viewed modulo a particular constant corresponds to [Z/nZ]
as defined abstractly in CyclicAxioms. *)

(** This library has been deprecated since Coq version 8.17. *)

(** Even if the construction provided here is not reused for building
the efficient arbitrary precision numbers, it provides a simple
implementation of CyclicAxioms, hence ensuring its coherence. *)
Expand Down