| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fix for Coq 8.4pl2 |  Jason Gross | 2016-11-12 |
| | | |||
| * | Fix Not_found exception in 8.4 | Jason Gross | 2016-11-03 |
| | | | | | | Caused by rewriting with a hypothesis with a type of the form [?1 x y] where [?1] is an evar. | ||
| * | 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 |