Skip to content

wip generic typing lemmas #474

wip generic typing lemmas

wip generic typing lemmas #474

Triggered via push November 16, 2023 16:12
Status Failure
Total duration 2m 16s
Artifacts

build.yml

on: push
Fit to window
Zoom out
Zoom in

Annotations

1 error and 10 warnings
build: theories/GenericTyping.v#L901
Syntax error: '@' expected after [term level 200] (in [term]).
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