Skip to content
Snippets Groups Projects

Normalize focused goal output

Merged 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

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
Please register or sign in to reply
Loading