• 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
Name
Last commit
Last update
algebra Loading commit data...
benchmark Loading commit data...
docs Loading commit data...
heap_lang Loading commit data...
prelude Loading commit data...
program_logic Loading commit data...
proofmode Loading commit data...
tests Loading commit data...
.gitignore Loading commit data...
.gitlab-ci.yml Loading commit data...
LICENSE Loading commit data...
Makefile Loading commit data...
ProofMode.md Loading commit data...
README.md Loading commit data...
_CoqProject Loading commit data...
naming.txt Loading commit data...