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 |