Deprecate renToWk, fix generic typing #477
This run and associated checks have been archived and are scheduled for deletion.
Learn more about checks retention
Annotations
1 error and 3 warnings
build:
theories/DeclarativeTyping.v#L133
Syntax error: ':' or '@' expected after [term level 50] (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
|