Pierre Roux

Adapt to https://github.com/coq/coq/pull/19310 This should be merged in sync with the upstream PR

Rename Coq requirement prefix to Stdlib

21

In anticipation of renaming to Rocq. For backward compatibility, "Coq" still works by being replaced on the fly with "Stdlib" and emiting a warning. - [x] Added / updated **test-suite**....

[CI] Remove one more dependency to MathComp 1

1

This was a fake dependency, QuickChick perfectly builds with MC2 but was kept on MC1 for some nasty menhir version kludge in ci-json. This copies in ci-json the menhir config...

[refman] Clarify parsing and notation interpretation phases

18

As a newcomer I remember having a hard time understanding the notation mechanism, particularly the distinction between lexing, parsing and notation interpretations. Let's avoid mixing those phases and clarify the...

Adapt to https://github.com/coq/coq/pull/19310 This should be merged in sync with the upstream PR

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

2

Adapt to https://github.com/coq/coq/pull/19310 This should be merged *only once upstream PR is merged*.

Adapt to https://github.com/coq/coq/pull/19530 This is an adaptation in anticipation of the day the temporary backward compatibility introduced in the upstream PR will be removed (probably a few years in the...

Adapt to https://github.com/coq/coq/pull/19530 This is an adaptation in anticipation of the day the temporary backward compatibility introduced in the upstream PR will be removed (probably a few years in the...