Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | key maps + small glitch hyp highlight/folding code. | Pierre Courtieu | 2018-06-11 |
| | |||
* | Changed the look of folding/unfolding hyps. | Pierre Courtieu | 2018-06-08 |
| | |||
* | Shorter CHANGES + smal fixes in hide/highlight hyps code. | Pierre Courtieu | 2018-06-04 |
| | |||
* | Click hypothesis to (un)hide them. | Pierre Courtieu | 2018-06-01 |
| | |||
* | Updated CHANGES about hiding and highlighting of hyps. | Pierre Courtieu | 2018-05-31 |
| | |||
* | Bind C-c C-m (= C-c RET) to proof-goto-point [tty] (#228) | Erik Martin-Dorel | 2018-02-20 |
| | | | Close ProofGeneral/PG#31 | ||
* | Prettier cheat face (background + box). | Pierre Courtieu | 2017-11-06 |
| | |||
* | Updating CHANGES with lexer extensibility. | Pierre Courtieu | 2017-10-26 |
| | |||
* | Remove default key-binding for proof-electric-terminator-toggle. | Erik Martin-Dorel | 2017-03-03 |
| | | | | Close ProofGeneral/PG#160 | ||
* | documentation and CHANGES for coq-compile-keep-going | Hendrik Tews | 2016-12-08 |
| | |||
* | write CHANGES | Hendrik Tews | 2016-11-30 |
| | |||
* | Update CHANGES. | Erik Martin-Dorel | 2016-10-16 |
| | | | | Related: ProofGeneral/PG#41 | ||
* | Detail. | Erik Martin-Dorel | 2016-09-18 |
| | |||
* | Promote CHANGES since 2820cb68 as related to PG 4.4. | Erik Martin-Dorel | 2016-09-18 |
| | |||
* | Adding the option to highlight susual symbols. | Pierre Courtieu | 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. | Pierre Courtieu | 2016-06-23 |
| | |||
* | updating CHANGES to the last commit. | Pierre Courtieu | 2016-03-21 |
| | |||
* | Cleaning CHANGES. | Pierre Courtieu | 2016-01-19 |
| | |||
* | updating CHANGES | Pierre Courtieu | 2016-01-06 |
| | |||
* | Updated the CHANGES files, mainly git url. | Pierre Courtieu | 2015-11-30 |
| | |||
* | proof-assert-command-hook added + Auto adjust width in coq mode. | Pierre Courtieu | 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. | Pierre Courtieu | 2015-06-23 |
| | |||
* | A command to set coq printing width smartly. | Pierre Courtieu | 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). | Pierre Courtieu | 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. | Pierre Courtieu | 2015-03-09 |
| | |||
* | Fixed stuff in CHANGES. | Pierre Courtieu | 2015-03-05 |
| | |||
* | Customization variables for modules, section and proof indentation. | Pierre Courtieu | 2015-03-05 |
| | |||
* | Fixed compilation issue with previous commit + CHANGE updates. | Pierre Courtieu | 2015-03-04 |
| | |||
* | coloring names in resposne and goals | Pierre Courtieu | 2015-02-03 |
| | |||
* | Fixed a bug in script navigation. Updated CHANGE | Pierre Courtieu | 2015-01-27 |
| | |||
* | changed default indentation of match's cases. | Pierre Courtieu | 2015-01-14 |
| | |||
* | Removing non-smie indentation + fix CHANGES. | Pierre Courtieu | 2015-01-09 |
| | |||
* | trying to indent pending forall in the expected way | Pierre Courtieu | 2015-01-05 |
| | |||
* | Supporting more bullets (coq 8.5), like ++ or ++++. | Pierre Courtieu | 2014-12-23 |
| | |||
* | * coq-smie.el (coq-smie-.-deambiguate): Proofs don't start with a definition. | Stefan Monnier | 2014-06-04 |
| | | | | | (coq-smie-backward-token): Don't burp at EOB. (coq-smie-rules): Indent top-level ":" like ":=". | ||
* | Fixing undeclared variables for compilation. | Pierre Courtieu | 2013-07-04 |
| | |||
* | Added an entry to CHANGEs about coq project fields. | Pierre Courtieu | 2013-06-21 |
| | |||
* | - implement proof-script insertion | Hendrik Tews | 2013-01-21 |
| | |||
* | document latest changes | Hendrik Tews | 2013-01-17 |
| | |||
* | - support bullets and braces in Prooftree | Hendrik Tews | 2013-01-15 |
| | | | | - prooftree protocol change to version 3 | ||
* | write CHANGES | Hendrik Tews | 2012-11-15 |
| | |||
* | Updates for PG 4.3 | David Aspinall | 2012-10-19 |
| | |||
* | Fixed a bug in three windows mode. | Pierre Courtieu | 2012-09-25 |
| | |||
* | Added one point + details to CHANGES. | Pierre Courtieu | 2012-09-07 |
| | |||
* | Fixed double hit terminator. Now it is disabled by default, and | Pierre Courtieu | 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. | David Aspinall | 2012-08-14 |
| | |||
* | Fixing compilation. Still need to verify some smie stuff on different ↵ | Pierre Courtieu | 2012-07-24 |
| | | | | versions of emacs. | ||
* | Added completion to insert Require, based on coq-load-path. | Pierre Courtieu | 2012-07-09 |
| | |||
* | updated CHANGES for Coq. | Pierre Courtieu | 2012-07-09 |
| | |||
* | More fixes in coq indentation. | Pierre Courtieu | 2012-07-06 |
| |