Skip to content
  • Robbert Krebbers's avatar
    Let set_solver not use eauto by default. · 9aff6bb6
    Robbert Krebbers authored
    In most cases there is a lot of duplicate proof search performed by
    both naive_solver and eauto. Especially since naive_solver calls its
    tactic (in the case of set_solver this used to be eauto) quite eagerly
    this made it very slow.
    Note that set_solver is this too slow and should be improved.