Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Bump version from 4.4.1~pre to 4.5-git | 2018-08-22 | |
| | | | | This commit ensures the version number is (version-to-list)-compliant. | ||
* | key maps + small glitch hyp highlight/folding code. | 2018-06-11 | |
| | |||
* | Changed the look of folding/unfolding hyps. | 2018-06-08 | |
| | |||
* | Shorter CHANGES + smal fixes in hide/highlight hyps code. | 2018-06-04 | |
| | |||
* | Click hypothesis to (un)hide them. | 2018-06-01 | |
| | |||
* | Updated CHANGES about hiding and highlighting of hyps. | 2018-05-31 | |
| | |||
* | Bind C-c C-m (= C-c RET) to proof-goto-point [tty] (#228) | 2018-02-20 | |
| | | | Close ProofGeneral/PG#31 | ||
* | Prettier cheat face (background + box). | 2017-11-06 | |
| | |||
* | Updating CHANGES with lexer extensibility. | 2017-10-26 | |
| | |||
* | Remove default key-binding for proof-electric-terminator-toggle. | 2017-03-03 | |
| | | | | Close ProofGeneral/PG#160 | ||
* | documentation and CHANGES for coq-compile-keep-going | 2016-12-08 | |
| | |||
* | write CHANGES | 2016-11-30 | |
| | |||
* | Update CHANGES. | 2016-10-16 | |
| | | | | Related: ProofGeneral/PG#41 | ||
* | Detail. | 2016-09-18 | |
| | |||
* | Promote CHANGES since 2820cb68 as related to PG 4.4. | 2016-09-18 | |
| | |||
* | Adding the option to highlight susual symbols. | 2016-07-22 | |
| | | | | | This may look ugly to the majority, so I let it off by default. I find it helpfull to have structuring symbols bold. | ||
* | Updating CHANGES. | 2016-06-23 | |
| | |||
* | updating CHANGES to the last commit. | 2016-03-21 | |
| | |||
* | Cleaning CHANGES. | 2016-01-19 | |
| | |||
* | updating CHANGES | 2016-01-06 | |
| | |||
* | Updated the CHANGES files, mainly git url. | 2015-11-30 | |
| | |||
* | proof-assert-command-hook added + Auto adjust width in coq mode. | 2015-10-12 | |
| | | | | | | | This hook was missing, it allows to send complete commands before the (set of) command(s) sent by the user. It shall be used when proof-shell-insert-hook cannot be used (because of multiple prompts appearing). | ||
* | Update to CHANGE. | 2015-06-23 | |
| | |||
* | A command to set coq printing width smartly. | 2015-03-26 | |
| | | | | | Set the width to the current goals window. Default binding: C-c C-a C-w. | ||
* | Added a command to send Queries to coq, with completion (C-c C-a C-q). | 2015-03-13 | |
| | | | | | Should replace C-c C-v at some point. Needs to have a complete list of such queries. Obeys C-u prefix for Printing all flag. | ||
* | Added bug fixes in CHANGES. | 2015-03-09 | |
| | |||
* | Fixed stuff in CHANGES. | 2015-03-05 | |
| | |||
* | Customization variables for modules, section and proof indentation. | 2015-03-05 | |
| | |||
* | Fixed compilation issue with previous commit + CHANGE updates. | 2015-03-04 | |
| | |||
* | coloring names in resposne and goals | 2015-02-03 | |
| | |||
* | Fixed a bug in script navigation. Updated CHANGE | 2015-01-27 | |
| | |||
* | changed default indentation of match's cases. | 2015-01-14 | |
| | |||
* | Removing non-smie indentation + fix CHANGES. | 2015-01-09 | |
| | |||
* | trying to indent pending forall in the expected way | 2015-01-05 | |
| | |||
* | Supporting more bullets (coq 8.5), like ++ or ++++. | 2014-12-23 | |
| | |||
* | * coq-smie.el (coq-smie-.-deambiguate): Proofs don't start with a definition. | 2014-06-04 | |
| | | | | | (coq-smie-backward-token): Don't burp at EOB. (coq-smie-rules): Indent top-level ":" like ":=". | ||
* | Fixing undeclared variables for compilation. | 2013-07-04 | |
| | |||
* | Added an entry to CHANGEs about coq project fields. | 2013-06-21 | |
| | |||
* | - implement proof-script insertion | 2013-01-21 | |
| | |||
* | document latest changes | 2013-01-17 | |
| | |||
* | - support bullets and braces in Prooftree | 2013-01-15 | |
| | | | | - prooftree protocol change to version 3 | ||
* | write CHANGES | 2012-11-15 | |
| | |||
* | Updates for PG 4.3 | 2012-10-19 | |
| | |||
* | Fixed a bug in three windows mode. | 2012-09-25 | |
| | |||
* | Added one point + details to CHANGES. | 2012-09-07 | |
| | |||
* | Fixed double hit terminator. Now it is disabled by default, and | 2012-09-05 | |
| | | | | | | | | enabling it disables electric-terminator and vice-versa. In case both are non nil at the same time, then electric teminator has priority. If people like it we may propose this to other modes than coq. + fixed window layout policy. | ||
* | Add user option proof-next-command-insert-space. | 2012-08-14 | |
| | |||
* | Fixing compilation. Still need to verify some smie stuff on different ↵ | 2012-07-24 | |
| | | | | versions of emacs. | ||
* | Added completion to insert Require, based on coq-load-path. | 2012-07-09 | |
| | |||
* | updated CHANGES for Coq. | 2012-07-09 | |
| |