changeset | a779402841f6 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Hooks for measuring how much interesting proving is going on in elaboration |
files |
changeset | 12b73f3c108e |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Switch to TDisjoint from CDisjoint; still need to implement obligation generation at EDisjoint uses |
files |
changeset | 6ee1c761818f |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Some small changes while failing to write [restrict] |
files |
changeset | 94ef20a31550 |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Fancier head normalization pushed inside of Disjoint |
files |
changeset | b4f2a258e52c |
---|---|
branch | |
bookmark | |
tag | |
user | Adam Chlipala <adamc@hcoop.net> |
description | Initial disjointness prover |
files |