• Robbert Krebbers's avatar
    Let set_solver not use eauto by default. · de5f0f84
    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.
    de5f0f84
sts.v 18.4 KB