Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Work around bad design in Coq | 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 | 2016-06-27 | |
| | |||
* | actually fix pose proof | 2016-06-25 | |
| | |||
* | s/fist/first/ | 2016-06-25 | |
| | |||
* | s/`proofgeneral`/Proof General/ | 2016-06-25 | |
| | |||
* | recommend pose proof instead of pose | 2016-06-25 | |
| | |||
* | s/on// | 2016-06-25 | |
| | |||
* | add closing parenthesis to "(and make" | 2016-06-25 | |
| | |||
* | s/quality/equality/ | 2016-06-25 | |
| | |||
* | s/be// | 2016-06-25 | |
| | |||
* | typo near "and make and" | 2016-06-25 | |
| | |||
* | wording change near "split this up" | 2016-06-25 | |
| | |||
* | add sigma type proof irrelevance wisdom from ssreflect | 2016-06-25 | |
| | |||
* | folkwisdom: remove redundant idtac | 2016-06-24 | |
| | |||
* | incorporate `Program Definition` match statement handling advice from @mattam82 | 2016-06-24 | |
| | |||
* | first draft of a "folk wisdom" document | 2016-06-24 | |