make key have sentences transparent to enable extraction in 8.20 #18
Annotations
10 warnings
|
theories/Core/HoareTriples.v#L107
with_spec does not respect the uniform inheritance condition
|
|
theories/Examples/TwoPhaseCommit/TwoPhaseParticipant.v#L212
Duplicate clear of Pre
|
|
theories/Examples/TwoPhaseCommit/TwoPhaseParticipant.v#L212
Duplicate clear of Pre
|
|
theories/Examples/TwoPhaseCommit/TwoPhaseParticipant.v#L362
Duplicate clear of Pre
|
|
theories/Examples/TwoPhaseCommit/TwoPhaseParticipant.v#L362
Duplicate clear of Pre
|
|
theories/Examples/TwoPhaseCommit/TwoPhaseInductiveInv.v#L820
Duplicate clear of G
|
|
theories/Examples/TwoPhaseCommit/TwoPhaseInductiveInv.v#L848
Duplicate clear of G
|
|
theories/Examples/TwoPhaseCommit/TwoPhaseInductiveInv.v#L870
Duplicate clear of G
|
|
theories/Examples/TwoPhaseCommit/TwoPhaseInductiveInv.v#L895
Duplicate clear of G
|
|
theories/Examples/Querying/QueryHooked.v#L250
Duplicate clear of CD
|
This job succeeded
Loading