| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Add more specific form of Proper_Let_In_nd_changebody |  Jason Gross | 2016-10-22 |
| | | |||
| * | Work around bug 5107 (broken return inference) | Jason Gross | 2016-10-03 |
| | | | | | | | This is https://coq.inria.fr/bugs/show_bug.cgi?id=5107, Unification got weaker in the past week or so. We work around this by making [dlet] non-dependent. | ||
| * | Fix a typo | Jason Gross | 2016-09-22 |
| | | |||
| * | Add a form of Let_In that carries a proof | Jason Gross | 2016-09-22 |
| | | |||
| * | alternative signing derivation |  Andres Erbsen | 2016-09-22 |
| | | | | | cleanup | ||
| * | Util.LetIn: fix proper instance | Andres Erbsen | 2016-09-22 |
| | | |||
| * | Change [Let ... in ...] to [dlet ... in ...] (#67) |  Jason Gross | 2016-09-19 |
| | | | | | For "definition". This fixes #65; [Let] conflicts with the vernacular [Let] in Coq 8.4. | ||
| * | Add reserved notation for Let, change # | Jason Gross | 2016-09-17 |
| | | | | | | We reserve [a # b] in Notations.v, and make it's level compatible with the notation declared in the std lib for Q. | ||
| * | deduplicate Let_In into src/Util/LetIn.v | Andres Erbsen | 2016-09-17 |
 |
index : fiat-crypto | |
| fast, formally verified cryptography |
| aboutsummaryrefslogtreecommitdiff |