Skip to content

Merge pull request #250 from peterlefanulumsdaine/adapt-notation-level #204

Merge pull request #250 from peterlefanulumsdaine/adapt-notation-level

Merge pull request #250 from peterlefanulumsdaine/adapt-notation-level #204

Triggered via push January 21, 2025 03:47
Status Success
Total duration 5m 1s
Artifacts
Matrix: build-typetheory
Fit to window
Zoom out
Zoom in

Annotations

19 warnings
Build with dev
"From Coq" has been replaced by "From Stdlib".
Build with dev
"From Coq" has been replaced by "From Stdlib".
Build with dev
Postfix notations (i.e. starting with a nonterminal symbol and
Build with dev
Closed notations (i.e. starting and ending with a terminal symbol)
Build with dev
Postfix notations (i.e. starting with a nonterminal symbol and
Build with dev
Postfix notations (i.e. starting with a nonterminal symbol and
Build with dev
Postfix notations (i.e. starting with a nonterminal symbol and
Build with dev
The '%' scope delimiter in 'Arguments' commands is deprecated, use
Build with dev
disp_nat_z_iso_to_trans does not respect the uniform inheritance
Build with latest
Postfix notations (i.e. starting with a nonterminal symbol and
Build with latest
Closed notations (i.e. starting and ending with a terminal symbol)
Build with latest
Postfix notations (i.e. starting with a nonterminal symbol and
Build with latest
Postfix notations (i.e. starting with a nonterminal symbol and
Build with latest
Postfix notations (i.e. starting with a nonterminal symbol and
Build with latest
The '%' scope delimiter in 'Arguments' commands is deprecated, use
Build with latest
disp_nat_z_iso_to_trans does not respect the uniform inheritance
Build with 8.16
Declaring arbitrary terms as hints is fragile; it is recommended to
Build with 8.16
Declaring arbitrary terms as hints is fragile; it is recommended to
Build with 8.16
disp_nat_z_iso_to_trans does not respect the uniform inheritance