Skip to content
  • Jacques-Henri Jourdan's avatar
    Improve iStartProof. · d7db5250
    Jacques-Henri Jourdan authored
    1- Avoid [type_term (eq_refl : @eq Type PROP PROP')] when [PROP] is not given. This has significant performance implications.
    2- In th case PROP is given (i.e., only when the tactic is manually used), introduce all the foralls and lets.
    d7db5250