Skip to content

Normalize focused goal output

Tej Chajed requested to merge tchajed/stdpp:adjust-focused-goal into master

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.

Merge request reports