Adapt to https://github.com/coq/coq/pull/19530 · coq-community/paramcoq@c048b42

Triggered via pull request September 17, 2024 09:59

proux01

opened #127

stdlib_repo

Status Success

Total duration 2m 43s

Artifacts –

docker-action.yml

on: pull_request

Matrix: build

8 warnings

The following actions use a deprecated Node.js version and will be forced to run on node20: actions/checkout@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/

Automatically putting I1 in Prop even though it was declared with

Automatically putting I2 in Prop even though it was declared with

Automatically putting I3 in Prop even though it was declared with

Automatically putting J in Prop even though it was declared with

Automatically putting K in Prop even though it was declared with

Not a truly recursive fixpoint.

"From Coq" has been replaced by "From Stdlib".