Merge pull request #10 from mit-pdos/fix-deprecations · mit-pdos/argosy@2926f18

Triggered via push April 1, 2026 13:02

tchajed

master

Status Success

Total duration 2m 3s

Artifacts –

coq-action.yml

on: push

Matrix: build

11 warnings

build (latest): vendor/array/src/Array.v#L491

Notations "_ [ _ := _ ]" defined at level 10 with arguments constr

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