Skip to content
CI (Coq, docker, dev)

Bump etc/coq-scripts from 8b66ebe to bbe2c4c #136

Sign in to view logs

Bump etc/coq-scripts from 8b66ebe to bbe2c4c

Bump etc/coq-scripts from 8b66ebe to bbe2c4c #136

Triggered via pull request October 6, 2023 13:34
@dependabotdependabot[bot]
opened #98
dependabot/submodules/etc/coq-scripts-bbe2c4c
Status Failure
Total duration 1m 27s
Artifacts –

docker-coq.yml

on: pull_request
build
1m 13s
build
Fit to window
Zoom out
Zoom in

Annotations

2 errors and 10 warnings
build: src/Common/Coq__8_4__8_5__Compat.v#L596
Syntax error: '.' expected after [gallina_ext] (in [vernac_aux]).
build: src/Common/Coq__8_4__8_5__Compat.v#L596
Syntax error: '.' expected after [gallina_ext] (in [vernac_aux]).
build: src/Common/Coq__8_4__8_5__Compat.v#L11
There is no flag or option with this name: "Template Check".
build: src/Common/Coq__8_4__8_5__Compat.v#L27
There is no flag or option with this name:
build: src/Common/Coq__8_4__8_5__Compat.v#L28
There is no flag or option with this name: "Apply With Renaming".
build: src/Common/Coq__8_4__8_5__Compat.v#L56
Use of “Require” inside a module is fragile. It is not recommended
build: src/Common/Coq__8_4__8_5__Compat.v#L57
Use of “Require” inside a module is fragile. It is not recommended
build: src/Common/Coq__8_4__8_5__Compat.v#L58
Use of “Require” inside a module is fragile. It is not recommended
build: src/Common/Coq__8_4__8_5__Compat.v#L59
Use of “Require” inside a module is fragile. It is not recommended
build: src/Common/Coq__8_4__8_5__Compat.v#L11
There is no flag or option with this name: "Template Check".
build: src/Common/Coq__8_4__8_5__Compat.v#L27
There is no flag or option with this name:
build: src/Common/Coq__8_4__8_5__Compat.v#L28
There is no flag or option with this name: "Apply With Renaming".