| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | Small example of bounds-calculation with dependent types (#61) |  Jason Gross | 2016-09-29 |
| * | Fix for Coq < 8.6 |  Jason Gross | 2016-09-22 |
| * | Add a non-higher-order syntax, and reg assignment |  Jason Gross | 2016-09-22 |
| * | Make the example a function for reification | Jason Gross | 2016-09-18 |
| * | Split off lemmas about [InlineConst] | Jason Gross | 2016-09-16 |
| * | Fixes for Coq 8.4 | Jason Gross | 2016-09-07 |
| * | Remove the need for coercions in well-typing of Reify | Jason Gross | 2016-09-07 |
| * | Key on the head of the operation in reification | Jason Gross | 2016-09-07 |
| * | Add Common Subexpression Elimination | Jason Gross | 2016-09-06 |
| * | Better implicit arguments for wf types | Jason Gross | 2016-09-05 |
| * | Add comments to WfReflective, handle Expr | Jason Gross | 2016-09-05 |
| * | Remove ReifyDirect | Jason Gross | 2016-09-05 |
| * | A helper lemma for [Wf] | Jason Gross | 2016-09-05 |
| * | PHOAS syntax | Jason Gross | 2016-09-05 |
 |
index : fiat-crypto | |
| fast, formally verified cryptography |
| aboutsummaryrefslogtreecommitdiff |