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