Skip to content
  • Tej Chajed's avatar
    Normalize focused goal output · 06c4277c
    Tej Chajed authored
    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.
    06c4277c