• 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
..
base.v Loading commit data...
bsets.v Loading commit data...
co_pset.v Loading commit data...
collections.v Loading commit data...
countable.v Loading commit data...
decidable.v Loading commit data...
error.v Loading commit data...
fin_collections.v Loading commit data...
fin_map_dom.v Loading commit data...
fin_maps.v Loading commit data...
finite.v Loading commit data...
functions.v Loading commit data...
gmap.v Loading commit data...
hashset.v Loading commit data...
hlist.v Loading commit data...
lexico.v Loading commit data...
list.v Loading commit data...
listset.v Loading commit data...
listset_nodup.v Loading commit data...
mapset.v Loading commit data...
natmap.v Loading commit data...
nmap.v Loading commit data...
numbers.v Loading commit data...
option.v Loading commit data...
orders.v Loading commit data...
pmap.v Loading commit data...
prelude.v Loading commit data...
pretty.v Loading commit data...
proof_irrel.v Loading commit data...
relations.v Loading commit data...
sets.v Loading commit data...
streams.v Loading commit data...
stringmap.v Loading commit data...
strings.v Loading commit data...
tactics.v Loading commit data...
vector.v Loading commit data...
zmap.v Loading commit data...