Skip to content
  • Robbert Krebbers's avatar
    Start improving control over type class search in proof mode tactics. · a74b8077
    Robbert Krebbers authored
    We do this in two ways:
    
    - Use `notypeclasses refine` instead of `eapply`, to avoid type class
      search being called arbitrary.
    - Use `typeclasses eauto` instead of `apply _`, to avoid type class
      search being called on unrelated evars.
    
    I mainly tried this for `iSpecialize` and friends; this same remains to
    be done for all other tactics.
    
    This commit also makes partial progress w.r.t. issue #135.
    a74b8077