dune config from Coq to Rocq, not mentioning -type-in-type - #257

Node.js 20 is deprecated. The following actions target Node.js 20 but are being forced to run on Node.js 24: actions/cache@v4, actions/checkout@v4. For more information see: https://github.blog/changelog/2025-09-19-deprecation-of-node-20-on-github-actions-runners/

Use of "Notation" keyword for abbreviations is deprecated, use

Use of "Notation" keyword for abbreviations is deprecated, use

Implicitly declaring hint databases is deprecated. Please explicitly

Use of "Notation" keyword for abbreviations is deprecated, use

Implicitly declaring hint databases is deprecated. Please explicitly

Use of "Notation" keyword for abbreviations is deprecated, use

Use of "Notation" keyword for abbreviations is deprecated, use

Postfix notations (i.e. starting with a nonterminal symbol and

Closed notations (i.e. starting and ending with a terminal symbol)