Skip to content
CI

CI #81

Sign in to view logs

CI

CI #81

Triggered via schedule May 26, 2026 09:12
@tchajedtchajed
⁠ 7617923
master
Status Success
Total duration 1m 46s
Artifacts –

coq-action.yml

on: schedule
Matrix: build
Fit to window
Zoom out
Zoom in

Annotations

20 warnings
build (dev): vendor/array/src/Array.v#L503
Implicitly declaring Rewrite hint databases is deprecated. Please
build (dev): vendor/array/src/Array.v#L492
Postfix notations (i.e. starting with a nonterminal symbol and
build (dev): vendor/array/src/Array.v#L491
Notations "_ [ _ := _ ]" defined at level 10 with arguments constr
build (dev): vendor/array/src/Array.v#L491
Postfix notations (i.e. starting with a nonterminal symbol and
build (dev): vendor/array/src/Array.v#L490
Postfix notations (i.e. starting with a nonterminal symbol and
build (dev): vendor/array/src/Array.v#L325
Implicitly declaring Rewrite hint databases is deprecated. Please
build (dev): vendor/array/src/Array.v#L267
Implicitly declaring Rewrite hint databases is deprecated. Please
build (dev): vendor/array/src/Array.v#L34
Implicitly declaring Rewrite hint databases is deprecated. Please
build (dev): vendor/array/src/Array.v#L18
Use of "Notation" keyword for abbreviations is deprecated, use
build (dev): vendor/classes/src/Default.v#L6
Use of "Notation" keyword for abbreviations is deprecated, use
build (latest): vendor/array/src/Array.v#L503
Implicitly declaring Rewrite hint databases is deprecated. Please
build (latest): vendor/array/src/Array.v#L492
Postfix notations (i.e. starting with a nonterminal symbol and
build (latest): vendor/array/src/Array.v#L491
Notations "_ [ _ := _ ]" defined at level 10 with arguments constr
build (latest): vendor/array/src/Array.v#L491
Postfix notations (i.e. starting with a nonterminal symbol and
build (latest): vendor/array/src/Array.v#L490
Postfix notations (i.e. starting with a nonterminal symbol and
build (latest): vendor/array/src/Array.v#L325
Implicitly declaring Rewrite hint databases is deprecated. Please
build (latest): vendor/array/src/Array.v#L267
Implicitly declaring Rewrite hint databases is deprecated. Please
build (latest): vendor/array/src/Array.v#L34
Implicitly declaring Rewrite hint databases is deprecated. Please
build (latest): vendor/array/src/Array.v#L18
Use of "Notation" keyword for abbreviations is deprecated, use
build (latest): vendor/classes/src/Default.v#L6
Use of "Notation" keyword for abbreviations is deprecated, use