Skip to content
LogRel CI

First changes to GenericTyping for locally irr types. #473

Sign in to view logs

First changes to GenericTyping for locally irr types.

First changes to GenericTyping for locally irr types. #473

Triggered via push November 16, 2023 15:55
@jpoiretjpoiret
pushed ac6c263
extension_types
Status Failure
Total duration 2m 20s
Artifacts –

build.yml

on: push
build
2m 8s
build
Fit to window
Zoom out
Zoom in

Annotations

1 error and 10 warnings
build: theories/GenericTyping.v#L815
(in proof redtywf_trans): Attempt to save an incomplete proof
build
Argument B was previously inferred to be in scope type_scope but is
build
Argument B was previously inferred to be in scope type_scope but is
build
Argument B was previously inferred to be in the empty scope stack
build: theories/AutoSubst/Ast.v#L1276
The default value for instance locality is currently "local" in a
build: theories/AutoSubst/Ast.v#L1278
The default value for instance locality is currently "local" in a
build: theories/AutoSubst/Ast.v#L1280
The default value for instance locality is currently "local" in a
build: theories/AutoSubst/Ast.v#L1282
The default value for instance locality is currently "local" in a
build: theories/AutoSubst/Ast.v#L1284
The default value for instance locality is currently "local" in a
build: theories/AutoSubst/Ast.v#L1286
The default value for instance locality is currently "local" in a
build: theories/AutoSubst/Ast.v#L1335
The default value for instance locality is currently "local" in a