| Commit message (Collapse) | Author | Age |
| |
|
|
|
|
| |
and finished encoding admits.
|
|
|
|
| |
function.
|
|
|
|
|
|
|
|
|
|
|
|
| |
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
```
|
|
|
|
| |
Also move a definition about words, with a TODO about location, into WordUtil.
|
|
|