Skip to content
  • Tej Chajed's avatar
    Report an error when iIntro fails to find a forall · fa0b270b
    Tej Chajed authored
    The error handling for `iIntro (?)` and similar tactics didn't correctly
    report failures when the goal couldn't be turned into a universal
    quantifier. This is something missing from !482 due to no test
    triggering the error.