| Commit message (Collapse) | Author | Age |
|
|
|
| |
that add up to a monoid
|
| |
|
|
|
|
|
|
|
|
|
|
| |
Moving the [scalar] argument to the beginning of [iter_op] makes
inference of the [Proper] lemmas a bit easier.
Making [Reflexive eq] come before [Reflexive Equivalence.equiv] allows
[setoid_rewrite] to work; since [setoid_rewrite] does more unfolding
than [rewrite], we no longer need to unfold things to make the [rewrite]
work.
|
|
|
|
| |
ExtendedCoordinates and Ed25519 to use it.
|
|
|
|
| |
CompleteEdwardsCurve/ExtendedCoordinates (we don't have testbit defined yet)
|
|\ |
|
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
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
```
|
| | |
|
|/ |
|
| |
|
|
|