| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-12-08 | documentation and CHANGES for coq-compile-keep-going | Hendrik Tews | |
| 2016-11-30 | write CHANGES | Hendrik Tews | |
| 2016-10-16 | Update CHANGES. | Erik Martin-Dorel | |
| Related: ProofGeneral/PG#41 | |||
| 2016-09-18 | Detail. | Erik Martin-Dorel | |
| 2016-09-18 | Promote CHANGES since 2820cb68 as related to PG 4.4. | Erik Martin-Dorel | |
| 2016-07-22 | Adding the option to highlight susual symbols. | Pierre Courtieu | |
| This may look ugly to the majority, so I let it off by default. I find it helpfull to have structuring symbols bold. | |||
| 2016-06-23 | Updating CHANGES. | Pierre Courtieu | |
| 2016-03-21 | updating CHANGES to the last commit. | Pierre Courtieu | |
| 2016-01-19 | Cleaning CHANGES. | Pierre Courtieu | |
| 2016-01-06 | updating CHANGES | Pierre Courtieu | |
| 2015-11-30 | Updated the CHANGES files, mainly git url. | Pierre Courtieu | |
| 2015-10-12 | proof-assert-command-hook added + Auto adjust width in coq mode. | Pierre Courtieu | |
| 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). | |||
| 2015-06-23 | Update to CHANGE. | Pierre Courtieu | |
| 2015-03-26 | A command to set coq printing width smartly. | Pierre Courtieu | |
| Set the width to the current goals window. Default binding: C-c C-a C-w. | |||
| 2015-03-13 | Added a command to send Queries to coq, with completion (C-c C-a C-q). | Pierre Courtieu | |
| 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. | |||
| 2015-03-09 | Added bug fixes in CHANGES. | Pierre Courtieu | |
| 2015-03-05 | Fixed stuff in CHANGES. | Pierre Courtieu | |
| 2015-03-05 | Customization variables for modules, section and proof indentation. | Pierre Courtieu | |
| 2015-03-04 | Fixed compilation issue with previous commit + CHANGE updates. | Pierre Courtieu | |
| 2015-02-03 | coloring names in resposne and goals | Pierre Courtieu | |
| 2015-01-27 | Fixed a bug in script navigation. Updated CHANGE | Pierre Courtieu | |
| 2015-01-14 | changed default indentation of match's cases. | Pierre Courtieu | |
| 2015-01-09 | Removing non-smie indentation + fix CHANGES. | Pierre Courtieu | |
| 2015-01-05 | trying to indent pending forall in the expected way | Pierre Courtieu | |
| 2014-12-23 | Supporting more bullets (coq 8.5), like ++ or ++++. | Pierre Courtieu | |
| 2014-06-04 | * coq-smie.el (coq-smie-.-deambiguate): Proofs don't start with a definition. | Stefan Monnier | |
| (coq-smie-backward-token): Don't burp at EOB. (coq-smie-rules): Indent top-level ":" like ":=". | |||
| 2013-07-04 | Fixing undeclared variables for compilation. | Pierre Courtieu | |
| 2013-06-21 | Added an entry to CHANGEs about coq project fields. | Pierre Courtieu | |
| 2013-01-21 | - implement proof-script insertion | Hendrik Tews | |
| 2013-01-17 | document latest changes | Hendrik Tews | |
| 2013-01-15 | - support bullets and braces in Prooftree | Hendrik Tews | |
| - prooftree protocol change to version 3 | |||
| 2012-11-15 | write CHANGES | Hendrik Tews | |
| 2012-10-19 | Updates for PG 4.3 | David Aspinall | |
| 2012-09-25 | Fixed a bug in three windows mode. | Pierre Courtieu | |
| 2012-09-07 | Added one point + details to CHANGES. | Pierre Courtieu | |
| 2012-09-05 | Fixed double hit terminator. Now it is disabled by default, and | Pierre Courtieu | |
| 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. | |||
| 2012-08-14 | Add user option proof-next-command-insert-space. | David Aspinall | |
| 2012-07-24 | Fixing compilation. Still need to verify some smie stuff on different ↵ | Pierre Courtieu | |
| versions of emacs. | |||
| 2012-07-09 | Added completion to insert Require, based on coq-load-path. | Pierre Courtieu | |
| 2012-07-09 | updated CHANGES for Coq. | Pierre Courtieu | |
| 2012-07-06 | More fixes in coq indentation. | Pierre Courtieu | |
| 2012-01-18 | Added some detail on the indentation limitation in the CHANGE. | Pierre Courtieu | |
| 2012-01-12 | Fix typo, mention HOL Light | David Aspinall | |
| 2012-01-04 | Add link to Prooftree download | David Aspinall | |
| 2012-01-03 | update CHANGES | Hendrik Tews | |
| 2011-12-23 | Will release 4.2 next, after all | David Aspinall | |
| 2011-12-07 | - protect proof-shell-handle-delayed-output against the case where | Hendrik Tews | |
| proof-shell-end-goals-regexp is defined but does not match - add coq setting for hiding additional subgoals | |||
| 2011-11-15 | Suggest PG 4.1.1 will be released next | David Aspinall | |
| 2011-10-14 | Bump doc version numbers to 4.2pre. | David Aspinall | |
| 2011-06-22 | coq-use-smie not enabled by default | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |