Skip to content
  • Tej Chajed's avatar
    Normalize focused goal output · fd8f6c52
    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+.
    
    Iris does not currently produce this output, since no test calls `Show`
    with shelved goals, but this future-proofs the test normalization.
    fd8f6c52