• Robbert Krebbers's avatar
    Improve solve_proper a bit. · b3d2ff9b
    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.
tactics.v 20.8 KB