Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Don't rely on autogenerated names | Jason Gross | 2017-06-05 |
| | | | | | | 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). | ||
* | Strip trailing whitespace | Jason Gross | 2017-06-02 |
| | | | | | | | With ```bash bash ./etc/coq-scripts/formatting/strip-trailing-whitespace.sh ``` | ||
* | rename-everything | Andres Erbsen | 2017-04-06 |
| | |||
* | use [positive] for [F] modulus, char_ge_C instead of char_gt_C | Andres Erbsen | 2017-03-02 |
| | |||
* | WIP | Andres Erbsen | 2017-03-02 |
| | |||
* | address some code review comments | Andres Erbsen | 2017-03-02 |
| | |||
* | split the algebra library; use fsatz more | Andres Erbsen | 2017-03-02 |
| | |||
* | fsatz, nsatz_solve_nonzero | Andres Erbsen | 2017-03-02 |
| | |||
* | use field_nsatz in CompleteEdwardsCurve.Pre | Andres Erbsen | 2017-03-02 |
| | |||
* | remove eq_dec from Monoid | Andres Erbsen | 2016-08-23 |
| | |||
* | remove field_algebra | Andres Erbsen | 2016-07-11 |
| | |||
* | Fix broken notations (hopefully) | Jason Gross | 2016-06-22 |
| | |||
* | use Local Obligation Tactic (8.5-compat) | Andres Erbsen | 2016-06-21 |
| | |||
* | remove trailing whitespace from src/ | Andres Erbsen | 2016-06-20 |
| | |||
* | move nsatz out of algebra, improve algebra, port CompleteEdwardsCurveTheorems | Andres Erbsen | 2016-06-17 |
| | |||
* | port edwards curve spec | Andres Erbsen | 2016-06-16 |
| | |||
* | consolidate and rename Edwards curve lemmas | Andres Erbsen | 2016-04-25 |
| | |||
* | point_eq_dec | Andres Erbsen | 2016-04-22 |
| | |||
* | nicer verify() derivation starter | Andres Erbsen | 2016-03-21 |
| | |||
* | Finish absolutizing imports | Jason Gross | 2016-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 ``` | ||
* | document field issue re-appearing | Andres Erbsen | 2016-02-12 |
| | |||
* | port some edwards curve theorems | Andres Erbsen | 2016-02-12 |