| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | 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 |
 |
index : fiat-crypto | |
| fast, formally verified cryptography |
| aboutsummaryrefslogtreecommitdiff |