| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2015-10-13 | Fixed coq-id-at-point. | Pierre Courtieu | |
| 2015-10-13 | proof-retract-command-hook added + more auto adjust width in coq mode. | 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-10-09 | Trying to not delete frames too eagerly when laying out. | Pierre Courtieu | |
| 2015-10-09 | Fixing 4096 character limit of scomint-send-input. | Pierre Courtieu | |
| Extended the fix of #453 (trac tracker) for emacs 25 (>=24 instead of = 24). | |||
| 2015-10-09 | Fixing < 25 use of window-frame (mandatory arg). | Pierre Courtieu | |
| 2015-10-06 | Put 'delete-selection t on coq-terminator-insert | Clément Pit--Claudel | |
| delete-selection-mode requires command that insert text to be annotated with a 'delete-selection property. | |||
| 2015-10-06 | Move .cvsignore to .gitignore | Clément Pit--Claudel | |
| 2015-10-06 | Trying to deal with debug mode. | Pierre Courtieu | |
| 2015-09-29 | colorizing hypothesis in compact mode. | Pierre Courtieu | |
| 2015-09-29 | Fixed #1 (Missing space in coq-insert-intros). | Pierre Courtieu | |
| Added a newline and removed the useless intros. | |||
| 2015-09-29 | Cleaned TODO file in coq/. | Pierre Courtieu | |
| 2015-09-25 | More Fixes when issuing commands from another buffer. | Pierre Courtieu | |
| 2015-09-25 | Fixed bug when issuing commands from another buffer than scripting one. | Pierre Courtieu | |
| Hooks modifying things in *goals* or *response* now try to operate on the right frame/windows. | |||
| 2015-09-22 | hyps highlighting now supports compact contexts (in coq trunk soon). | Pierre Courtieu | |
| 2015-06-23 | Added a moderate support for double quotes in -arg lines of _CoqProject. | Pierre Courtieu | |
| 2015-06-23 | Update to CHANGE. | Pierre Courtieu | |
| 2015-05-19 | robustify last commit (disabling smie show-paren). | Pierre Courtieu | |
| 2015-05-19 | Disable smie parenthesis blink. Too slow sometimes. | Pierre Courtieu | |
| 2015-05-07 | Fixes #492. fixed regexp (\\< --> \\_< everywhere). | Pierre Courtieu | |
| Surprising that this did not raise before... | |||
| 2015-05-07 | Fixes #484. Added syntax. | Pierre Courtieu | |
| 2015-05-07 | Fixes #485. | Pierre Courtieu | |
| 2015-05-07 | Fixes #486 with an option. | Pierre Courtieu | |
| 2015-05-07 | Yet another half fix of smie lexer. | Pierre Courtieu | |
| || is either a boolean operator or a tactical. | |||
| 2015-04-27 | Fixed at-point detection (bis). | Pierre Courtieu | |
| 2015-04-27 | Fixed at-point detection. | Pierre Courtieu | |
| 2015-04-14 | bold unicode biders + Fixing highlighting in goals and response buffers + ↵ | Pierre Courtieu | |
| cleaning. | |||
| 2015-04-13 | Debugging font-lock for ∀, ∃, and λ. | Pierre Courtieu | |
| 2015-04-10 | Added unicode forall in font-lock regexps. | Pierre Courtieu | |
| 2015-04-07 | Added comment. | Pierre Courtieu | |
| 2015-04-07 | Fixed coq-id definition to be correct wrt to coq grammar. | Pierre Courtieu | |
| 2015-04-07 | Fixed highlighting of evars. | Pierre Courtieu | |
| 2015-04-03 | Trying to prepare indentation cleaning... | Pierre Courtieu | |
| 2015-04-02 | Highlighting stuff in goals mode (C-c C-a C-h). Very basic for now. | Pierre Courtieu | |
| 2015-04-01 | Fix fill-paragraph merging comments and code (never fill code). | Pierre Courtieu | |
| 2015-03-31 | Fixed smie code for ";" + added || in grammar. | Pierre Courtieu | |
| Actually || and + are overloaded and I don"t see how to deambiguate them. Indetation may be buggy until I found away. | |||
| 2015-03-27 | Fixed a small bug in indentation. | Pierre Courtieu | |
| 2015-03-27 | Fix disable evar colorizing in coq file. | Pierre Courtieu | |
| 2015-03-27 | Fixed a regex for detecting ids at point. | Pierre Courtieu | |
| 2015-03-26 | Colorizing hyps names robustified. Still incomplete. | 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-26 | A remark about project file in the documentation. | Pierre Courtieu | |
| Saying that one -arg should be followed by only one option. For several options, put several -arg, ONE PER LINE. | |||
| 2015-03-26 | Fixed a smal bug in colorizing response buffer. | Pierre Courtieu | |
| First constructor of an inductive was colorized as a hyp name. Hyp name colorizing should be done another way. Using font-lock here is probably bad. | |||
| 2015-03-24 | Fixed indetation of tryif then else. | Pierre Courtieu | |
| 2015-03-24 | fixed gfail hilighting. | Pierre Courtieu | |
| 2015-03-24 | added some keywords | Pierre Courtieu | |
| 2015-03-23 | Highlighting evars. | Pierre Courtieu | |
| 2015-03-23 | Fixed lazymatch and multimatch indentation/highlighting. | Pierre Courtieu | |
| 2015-03-13 | Summary: remove non-BSD cp arg | David Aspinall | |
| 2015-03-13 | Update dates for release next month | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |