aboutsummaryrefslogtreecommitdiffhomepage
path: root/CHANGES
Commit message (Collapse)AuthorAge
* Bump version from 4.4.1~pre to 4.5-gitGravatar Erik Martin-Dorel2018-08-22
| | | | This commit ensures the version number is (version-to-list)-compliant.
* key maps + small glitch hyp highlight/folding code.Gravatar Pierre Courtieu2018-06-11
|
* Changed the look of folding/unfolding hyps.Gravatar Pierre Courtieu2018-06-08
|
* Shorter CHANGES + smal fixes in hide/highlight hyps code.Gravatar Pierre Courtieu2018-06-04
|
* Click hypothesis to (un)hide them.Gravatar Pierre Courtieu2018-06-01
|
* Updated CHANGES about hiding and highlighting of hyps.Gravatar Pierre Courtieu2018-05-31
|
* Bind C-c C-m (= C-c RET) to proof-goto-point [tty] (#228)Gravatar Erik Martin-Dorel2018-02-20
| | | Close ProofGeneral/PG#31
* Prettier cheat face (background + box).Gravatar Pierre Courtieu2017-11-06
|
* Updating CHANGES with lexer extensibility.Gravatar Pierre Courtieu2017-10-26
|
* Remove default key-binding for proof-electric-terminator-toggle.Gravatar Erik Martin-Dorel2017-03-03
| | | | Close ProofGeneral/PG#160
* documentation and CHANGES for coq-compile-keep-goingGravatar Hendrik Tews2016-12-08
|
* write CHANGESGravatar Hendrik Tews2016-11-30
|
* Update CHANGES.Gravatar Erik Martin-Dorel2016-10-16
| | | | Related: ProofGeneral/PG#41
* Detail.Gravatar Erik Martin-Dorel2016-09-18
|
* Promote CHANGES since 2820cb68 as related to PG 4.4.Gravatar Erik Martin-Dorel2016-09-18
|
* Adding the option to highlight susual symbols.Gravatar Pierre Courtieu2016-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.Gravatar Pierre Courtieu2016-06-23
|
* updating CHANGES to the last commit.Gravatar Pierre Courtieu2016-03-21
|
* Cleaning CHANGES.Gravatar Pierre Courtieu2016-01-19
|
* updating CHANGESGravatar Pierre Courtieu2016-01-06
|
* Updated the CHANGES files, mainly git url.Gravatar Pierre Courtieu2015-11-30
|
* proof-assert-command-hook added + Auto adjust width in coq mode.Gravatar Pierre Courtieu2015-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.Gravatar Pierre Courtieu2015-06-23
|
* A command to set coq printing width smartly.Gravatar Pierre Courtieu2015-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).Gravatar Pierre Courtieu2015-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.Gravatar Pierre Courtieu2015-03-09
|
* Fixed stuff in CHANGES.Gravatar Pierre Courtieu2015-03-05
|
* Customization variables for modules, section and proof indentation.Gravatar Pierre Courtieu2015-03-05
|
* Fixed compilation issue with previous commit + CHANGE updates.Gravatar Pierre Courtieu2015-03-04
|
* coloring names in resposne and goalsGravatar Pierre Courtieu2015-02-03
|
* Fixed a bug in script navigation. Updated CHANGEGravatar Pierre Courtieu2015-01-27
|
* changed default indentation of match's cases.Gravatar Pierre Courtieu2015-01-14
|
* Removing non-smie indentation + fix CHANGES.Gravatar Pierre Courtieu2015-01-09
|
* trying to indent pending forall in the expected wayGravatar Pierre Courtieu2015-01-05
|
* Supporting more bullets (coq 8.5), like ++ or ++++.Gravatar Pierre Courtieu2014-12-23
|
* * coq-smie.el (coq-smie-.-deambiguate): Proofs don't start with a definition.Gravatar Stefan Monnier2014-06-04
| | | | | (coq-smie-backward-token): Don't burp at EOB. (coq-smie-rules): Indent top-level ":" like ":=".
* Fixing undeclared variables for compilation.Gravatar Pierre Courtieu2013-07-04
|
* Added an entry to CHANGEs about coq project fields.Gravatar Pierre Courtieu2013-06-21
|
* - implement proof-script insertionGravatar Hendrik Tews2013-01-21
|
* document latest changesGravatar Hendrik Tews2013-01-17
|
* - support bullets and braces in ProoftreeGravatar Hendrik Tews2013-01-15
| | | | - prooftree protocol change to version 3
* write CHANGESGravatar Hendrik Tews2012-11-15
|
* Updates for PG 4.3Gravatar David Aspinall2012-10-19
|
* Fixed a bug in three windows mode.Gravatar Pierre Courtieu2012-09-25
|
* Added one point + details to CHANGES.Gravatar Pierre Courtieu2012-09-07
|
* Fixed double hit terminator. Now it is disabled by default, andGravatar Pierre Courtieu2012-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.Gravatar David Aspinall2012-08-14
|
* Fixing compilation. Still need to verify some smie stuff on different ↵Gravatar Pierre Courtieu2012-07-24
| | | | versions of emacs.
* Added completion to insert Require, based on coq-load-path.Gravatar Pierre Courtieu2012-07-09
|
* updated CHANGES for Coq.Gravatar Pierre Courtieu2012-07-09
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-03 11:41:47 +0000