| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | use [positive] for [F] modulus, char_ge_C instead of char_gt_C |  Andres Erbsen | 2017-03-02 |
| * | Fix for Coq 8.4pl2 |  Jason Gross | 2016-11-12 |
| * | Fix Not_found exception in 8.4 | Jason Gross | 2016-11-03 |
| * | fix and prove ERepDec_correct | Andres Erbsen | 2016-11-02 |
| * | prove admit about F.to_nat x mod m | Andres Erbsen | 2016-10-27 |
| * | prove SRepMul admit | Andres Erbsen | 2016-10-25 |
| * | Fix for Coq 8.4 | Jason Gross | 2016-10-13 |
| * | refactor scalar multiplication thoery, implement SRepERepMul | Andres Erbsen | 2016-10-12 |
| * | integrate bitwise operations | Andres Erbsen | 2016-10-12 |
| * | generalize equiv relations in Util.Option and EdDSARepChange | Andres Erbsen | 2016-10-12 |
| * | move eddsa rep change | Andres Erbsen | 2016-09-22 |
 |
index : fiat-crypto | |
| fast, formally verified cryptography |
| aboutsummaryrefslogtreecommitdiff |