Olivier Laurent

[stdlib] Add properties and predicates on lists with output in Type

45

Add computational content to `List.v`: mainly `Type` is used instead of `Prop` as much as possible. **Kind:** feature. - [ ] Entry added in the changelog

Broken \ref in Section 6.2

1

The following link looks broken: https://github.com/math-comp/mcb/blob/c32cc2cada2c123d44b4f345f3812e3b199d478b/tex/chTypeInference.tex#L240 [Page 118](https://zenodo.org/record/3999478): `Chapter ??`.

Adapt to Rocq 9.0 with prefix "From Stdlib" for the standard library thus loosing compatibility with previous Coq versions but more robust for future versions.

Add attribute to restrict execution to specified Coq versions

3

I would be happy to have some attribute to control in which Coq versions some commands are executed in the spirit of a preprocessor directive. This could help in particular...

I don't know about dune building but concerning make building, this seems to be enough to work with Rocq 9 without compatibility shims. Since the installation [opam file](https://raw.githubusercontent.com/rocq-prover/opam/refs/heads/master/released/packages/coq-aac-tactics/coq-aac-tactics.8.20.0/opam) seems to...