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