aboutsummaryrefslogtreecommitdiff
path: root/src/Util/CaseUtil.v
Commit message (Collapse)AuthorAge
* 8.5 fixesGravatar Jason Gross2016-06-10
|
* moved lemmas from ModularBaseSystemProofs to various Util filesGravatar jadep2016-04-20
|
* Finish absolutizing importsGravatar Jason Gross2016-03-10
| | | | | | | | | | | | The file coqprime/Coqprime/ListAux.v was importing List, which was confusing machines on which mathclasses was also installed. Using https://github.com/JasonGross/coq-tools ```bash make -kj10 cd src git ls-files "*.v" | xargs python ~/Documents/repos/coq-tools/absolutize-imports.py -i -R . Crypto ```
* ModularBaseSystem.carry: implement, state lemmas, some progress on proofsGravatar Andres Erbsen2015-11-17