Pierre Roux
Pierre Roux
Following a discussion in https://github.com/math-comp/math-comp/pull/1195#discussion_r1549904498 among other.
C.f. https://github.com/math-comp/math-comp/pull/1179#discussion_r1516857538
Add a warning for notations with incompatible common prefixes, for instance ```Coq Reserved Notation "#0 #1" (at level 30). Reserved Notation "#0 #1 #2" (at level 40). (* Warning: Notations...
In a PR on master, call [dev/tools/update-compat.py](https://github.com/coq/coq/tools/update-compat.py) with the --release flag; this sets up Coq to support three -compat flag arguments including the upcoming one (instead of four). To ensure...
Following https://github.com/coq/coq/issues/18882 : * Once the final list of features is known, in a PR on master to be backported, generate the release changelog by calling [dev/tools/generate-release-changelog.sh](https://github.com/coq/coq/tools/generate-release-changelog.sh) and include it...
https://github.com/coq-community/coq-nix-toolbox/pull/245
Diff is not very readable so here is a sumup of the change in packages that are available with default mathcomp ``` 8.16 - coq-bits - coqeal - deriving -...
Adapt to https://github.com/coq/coq/pull/19310 This should be merged in sync with the upstream PR