| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
|
| |
This fixes all of the private-names warnings emitted by
compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus
the ones in coqprime, which I didn't touch).
|
| |
|
|
|
|
|
| |
With
```bash
bash ./etc/coq-scripts/formatting/strip-trailing-whitespace.sh
```
|
| | |
|
| |
|
|
|
|
|
|
|
|
|
|
|
|
| |
* hopefully all proofs we need about xzladderstep
* Better automation in xzproofs
* Speed up xzproofs with heuristic clearing
* Remove useless hypotheses
* XZProofs cleanup
* fix "group by isomorphism" proofs, use in XZProofs
|
| | |
|
| |
|
|
|
| |
We also need to stuff the local notations in a scope so that we can
still access the notations in core_scope
|
| | |
|
| | |
|
| |
|
Jason Gross
Andres Erbsen