Normalize focused goal output
Status | Pipeline | Created by | Stages | |
---|---|---|---|---|
Passed 00:11:22
| Stage: build |
Download artifacts
No artifacts found |
Merge the "1 focused goal" line with the subsequent "(shelved: 1)" line, since this is the new output in Coq 8.15+.
std++ does not currently produce this output, since no test calls Show
with shelved goals, but this future-proofs the test normalization.
Status | Pipeline | Created by | Stages | |
---|---|---|---|---|
Passed 00:11:22
| Stage: build |
Download artifacts
No artifacts found |