constructor sup of W can be well directed #459
kyoDralliam
This run and associated checks have been archived and are scheduled for deletion.
Learn more about checks retention
Annotations
10 warnings
|
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/DirectedDirections.v#L37
Unused variable d2 catches more than one case.
|
|
build:
theories/DirectedDirectioning.v#L11
The only parsing modifier has no effect in Reserved Notation.
|
|
build:
theories/DirectedDirectioning.v#L12
The only parsing modifier has no effect in Reserved Notation.
|
|
build:
theories/DirectedDirectioning.v#L13
The only parsing modifier has no effect in Reserved Notation.
|
|
build:
theories/DirectedTyping.v#L10
The only parsing modifier has no effect in Reserved Notation.
|
|
build:
theories/DirectedTyping.v#L11
The only parsing modifier has no effect in Reserved Notation.
|
|
build:
theories/DirectedTyping.v#L12
The only parsing modifier has no effect in Reserved Notation.
|