• Robbert Krebbers's avatar
    Let set_solver not use eauto by default. · 060c2b8f
    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.
    060c2b8f
collections.v 27.9 KB