• Dan Frumin's avatar
    A common rel_pure_l/r tactic utilizing typeclass search · d7cada37
    Dan Frumin authored
    - The typeclass `PureExec e1 e2` controls pure deterministic
      reductions
    - General tactics rel_pure_l and rel_pure_r that depend on that typeclass
    - The same typeclass can be used for WP tactics and tp tactics, potentially
    d7cada37
_CoqProject 1.11 KB