| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Work around bad design in Coq |  Jason Gross | 2016-07-19 |
| | | | | | | This is https://coq.inria.fr/bugs/show_bug.cgi?id=4949, [intuition] should not use [auto with *] by default | ||
| * | Update folkwisdom.md |  Andres Erbsen | 2016-06-27 |
| | | |||
| * | actually fix pose proof |  Andres Erbsen | 2016-06-25 |
| | | |||
| * | s/fist/first/ | Andres Erbsen | 2016-06-25 |
| | | |||
| * | s/`proofgeneral`/Proof General/ | Andres Erbsen | 2016-06-25 |
| | | |||
| * | recommend pose proof instead of pose | Andres Erbsen | 2016-06-25 |
| | | |||
| * | s/on// | Andres Erbsen | 2016-06-25 |
| | | |||
| * | add closing parenthesis to "(and make" | Andres Erbsen | 2016-06-25 |
| | | |||
| * | s/quality/equality/ | Andres Erbsen | 2016-06-25 |
| | | |||
| * | s/be// | Andres Erbsen | 2016-06-25 |
| | | |||
| * | typo near "and make and" | Andres Erbsen | 2016-06-25 |
| | | |||
| * | wording change near "split this up" | Andres Erbsen | 2016-06-25 |
| | | |||
| * | add sigma type proof irrelevance wisdom from ssreflect | Andres Erbsen | 2016-06-25 |
| | | |||
| * | folkwisdom: remove redundant idtac | Andres Erbsen | 2016-06-24 |
| | | |||
| * | incorporate `Program Definition` match statement handling advice from @mattam82 | Andres Erbsen | 2016-06-24 |
| | | |||
| * | first draft of a "folk wisdom" document | Andres Erbsen | 2016-06-24 |
 |
index : fiat-crypto | |
| fast, formally verified cryptography |
| aboutsummaryrefslogtreecommitdiff |
path: root/folkwisdom.md