make key have sentences transparent to enable extraction in 8.20 #18
+5
−5
Annotations
10 warnings
theories/Core/HoareTriples.v#L107
with_spec does not respect the uniform inheritance condition.
|
theories/Core/While.v#L10
The default and global localities for this command outside sections
|
theories/Examples/LockResource/ResourceProtocol.v#L6
The default and global localities for this command outside sections
|
theories/Examples/LockResource/LockProtocol.v#L6
The default and global localities for this command outside sections
|
theories/Examples/Greeter/Greeter.v#L7
The default and global localities for this command outside sections
|
theories/Examples/TwoPhaseCommit/TwoPhaseProtocol.v#L7
The default and global localities for this command outside sections
|
theories/Examples/TwoPhaseCommit/TwoPhaseParticipant.v#L212
Duplicate clear of Pre. Use {}Pre instead of {Pre}Pre
|
theories/Examples/TwoPhaseCommit/TwoPhaseParticipant.v#L212
Duplicate clear of Pre. Use {}Pre instead of {Pre}Pre
|
theories/Examples/TwoPhaseCommit/TwoPhaseParticipant.v#L362
Duplicate clear of Pre. Use {}Pre instead of {Pre}Pre
|
theories/Examples/TwoPhaseCommit/TwoPhaseParticipant.v#L362
Duplicate clear of Pre. Use {}Pre instead of {Pre}Pre
|
This job succeeded
Loading