Pierre Roux

Avoid thinks like ````Coq #[export] Set Warnings "-overwriting-delimiting-key". ``` that we had to do in https://github.com/math-comp/math-comp/pull/1157 because of a previous one in Coq's ssr files.

Fix the scope of arguments of intmul

6

So that 42%:~R parses to (intmul 1 (Posz 42)) rather than (intmul 1 (GRing.natmul 1 42)). ##### Motivation for this change ##### Things done/to do - [x] added corresponding entries...

Check MC1 backports

2

Check the TODO: MC1 label and backport missing PRs.

Ring coercions

17

##### Motivation for this change This is a draft pull request to experiment with https://github.com/LPCIC/coq-elpi/pull/484 This requires a custom branch of Coq https://github.com/proux01/coq/tree/dir with a prototype for directionality hints in...

Adapt to https://github.com/coq/coq/pull/17876

Port to MathComp 2

43

Requires https://github.com/jasmin-lang/coqword/pull/22

C.f. https://coq.zulipchat.com/#narrow/stream/237868-Hierarchy-Builder-devs-.26-users/topic/Extending.20the.20topology.20heirarchy/near/344790913

Boost stdlib development

36

This is a CEP to discuss the technical details of the corresponding point of the roadmap https://github.com/coq/ceps/blob/coq-roadmap/text/069-coq-roadmap.md Rendered: https://github.com/proux01/ceps/blob/boost-stdlib-dev/text/083-boost-stdlib-dev/text.md

Release 8.20

3

# Release checklist # ## When the release managers for version `X.X` get nominated ## - [x] Create a new issue to track the release process where you can copy-paste...

Clarify warning about Let/Variable/Hypothesis outside sections and turn it as error by default

6

This follows a discussion in https://github.com/coq/coq/pull/13445#discussion_r1526478233 - [x] Added / updated **test-suite**. - [x] Added **changelog**. - [x] Added / updated **documentation**. - [x] Documented any new / changed **user...