• Robbert Krebbers's avatar
    Improve solve_proper a bit. · f632ebfc
    Robbert Krebbers authored
    This is very experimental. It should now deal better with stuff like:
    
      match x with .. end = match y with .. end
    
    In case there is a hypothesis H : R x y, it will try to destruct it.
    f632ebfc
tactics.v 20.8 KB