| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2016-08-14 | Replace "Set Implicit Arguments" option with "Set Printing Implicit". | Erik Martin-Dorel | |
| Closes #99. | |||
| 2016-08-14 | Add Reserved Infix like Reserved Notation (#95) | Jason Gross | |
| 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-07-03 | Highlight Existing Class like Existing Instance (#85) | Jason Gross | |
| Closes #81 | |||
| 2016-07-01 | Highlight [nra] like [nia] and [lia] and [lra] (#84) | Jason Gross | |
| 2016-06-23 | Fix a typo | Clément Pit--Claudel | |
| 2016-06-23 | par-compile: Don't try to compile plugins (cm.*) | Clément Pit--Claudel | |
| 2016-06-23 | Fix a type error hidden until recent emacs. | Pierre Courtieu | |
| 2016-06-23 | Coq: option to prefer top over bottom of concl. | Pierre Courtieu | |
| 2016-06-10 | Color lia, romega, nia, psatz, nsatz, lra | Jason Gross | |
| This closes #77 | |||
| 2016-06-08 | abbrev twivking. | Pierre Courtieu | |
| 2016-06-08 | Fixing font-locking of unicode forall etc. | Pierre Courtieu | |
| 2016-05-27 | Fixing a smal glitch in indentation. | Pierre Courtieu | |
| 2016-05-20 | Merge branch 'master' of github.com:ProofGeneral/PG | Pierre Courtieu | |
| 2016-05-20 | Fix #72+ make user keywords prioritized over default ones. | Pierre Courtieu | |
| 2016-05-19 | Fail silently if Coq's version can't be detected | Clément Pit--Claudel | |
| Rationale: if Coq isn't installed, we will detect it when trying to run it, and we don't need to duplicate the error logic. Additionally, change from using process-lines to using shell-command, possibly through file-name-handler. The reason for this change is that we want to do the version detection on the remote server if we're running in Tramp. | |||
| 2016-05-16 | Merge branch 'master' of github.com:ProofGeneral/PG | Clément Pit--Claudel | |
| 2016-05-16 | Don't offer "" as the default in C-c C-c C-a | Clément Pit--Claudel | |
| 2016-05-16 | coq-syntax: Add a debug spec | Clément Pit--Claudel | |
| 2016-05-02 | Merge branch 'master' of github.com:ProofGeneral/PG | Pierre Courtieu | |
| 2016-05-02 | Fixing detection of symbol at point. | Pierre Courtieu | |
| Quote at start of a word should not be considered part of the word. Other characters than ' or _ are punctuation. | |||
| 2016-04-25 | Don't use string-empty-p | Clément Pit--Claudel | |
| It's too recent | |||
| 2016-04-14 | Respect user settings in coq-insert-intros | Clément Pit--Claudel | |
| Fixes #67. | |||
| 2016-03-21 | Option to toggle optimising response windo heigth. | Pierre Courtieu | |
| 2016-03-09 | Adding more keywords (Local xxx). | Pierre Courtieu | |
| 2016-03-09 | Fixed #64 again. e2c5da0 commits was wrong. | Pierre Courtieu | |
| 2016-03-09 | Fix #47. | Pierre Courtieu | |
| There are many other issued with coq-smie-forward-token. | |||
| 2016-03-09 | Fix #64. Use syntax-ppss in fill-nobreak-predicate. | Pierre Courtieu | |
| More robust to font-lock tweaks that change font inside comments (whitespace mode etc). | |||
| 2016-03-09 | Fixing a small glitch in indentation. | Pierre Courtieu | |
| if a "; tactic" is not at the end of its line, (hanging) then it should not act on indetation of next line. | |||
| 2016-03-09 | Fix #63 (efficiency pb in indentation). | Pierre Courtieu | |
| 2016-03-08 | Fixing #62. | Pierre Courtieu | |
| I don't know if it is a coq bug that bullet do not support Time. I remove Time from bullets for the moment. | |||
| 2016-03-08 | Avoiding useless computation in indentation code. | Pierre Courtieu | |
| 2016-03-08 | Should fix #49 and #55 (compilation of From .. Require). | Pierre Courtieu | |
| 2016-03-08 | Small fix for -Q options in loadpath. | Pierre Courtieu | |
| 2016-03-05 | Highlight ltac:(), constr:(), and uconstr:() | Clément Pit--Claudel | |
| Also refactor coq-font-lock-keywords-1 slightly. | |||
| 2016-02-29 | Redo 11b03d4 (ensure that ‘Time’ isn't added to internal commands) | Clément Pit--Claudel | |
| 2016-02-28 | Remove leftover comment | Clément Pit--Claudel | |
| 2016-02-28 | Don't add the ‘Time’ prefix to internal Coq commands | Clément Pit--Claudel | |
| This ensures that parts of Proof General that use Coq commands in the background are not confused by extra timing information. | |||
| 2016-02-27 | Add uconstr to the (ltac constr) list in SMIE | Clément Pit--Claudel | |
| 2016-02-27 | Fix a typo: s/coq-modulestart-proofstart/coq-indent-proofstart/ | Clément Pit--Claudel | |
| 2016-02-27 | Add a :safe predicate to indentation variables | Clément Pit--Claudel | |
| This is useful if people want to set them project-locally. | |||
| 2016-02-18 | Adding missing keywords | Pierre Courtieu | |
| 2016-02-17 | Merge pull request #40 from hendriktews/proof-tree | Pierre Courtieu | |
| basic proof tree changes for Coq 8.5 | |||
| 2016-02-06 | Ensure that version detection does not fail in 24.3 | Clément Pit--Claudel | |
| 2016-02-06 | Use coq-prog-name to autodetect version number | Clément Pit--Claudel | |
| 2016-01-27 | Fixed recent coq syntax change (tac !H become tac (H)). | Pierre Courtieu | |
| 2016-01-24 | basic proof tree changes for Coq 8.5 | Hendrik Tews | |
| Fixes to get basic proof tree functionality, including support for give_up, cycle, swap, revgoals. Unshelve and evar's don't work yet, see proof-tree issues #1 and #2 | |||
| 2016-01-19 | fix #36. | Pierre Courtieu | |
| 2016-01-14 | Add a few comments to explain values of coq-load-path | Clément Pit--Claudel | |
| 2016-01-14 | Mark coq-load-path-include-current as obsolete | Clément Pit--Claudel | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |