aboutsummaryrefslogtreecommitdiffstats
path: root/src/hls/HashTree.v
Commit message (Expand)AuthorAgeFilesLines
* Update to Coq 8.17 and CompCert 3.12Yann Herklotz2023-04-271-2/+2
* Work on proof of norm_expressionYann Herklotz2023-02-221-9/+83
* [sched] Remove some unprovable lemmasYann Herklotz2022-10-061-0/+20
* Work on implementing abstract predicatesYann Herklotz2022-07-191-0/+26
* Add work on abstract predicatesYann Herklotz2022-07-141-7/+4
* [sched] Remove unnecessary importsYann Herklotz2021-10-121-11/+0
* [sched] Add more lemmas into HashTreeYann Herklotz2021-10-121-0/+36
* [sched] Add HashTree.v for hashing arbitrary valuesYann Herklotz2021-10-121-0/+413