Skip to content
Snippets Groups Projects
  1. Nov 13, 2021
  2. Oct 13, 2021
    • 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.
      Verified
      06c4277c
  3. Jan 13, 2021
  4. Dec 10, 2020
  5. Nov 01, 2018
  6. Jun 25, 2018
Loading