Skip to content
  • 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.
    b3d2ff9b