aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* abbrev twivking.Gravatar Pierre Courtieu2016-06-08
|
* Fixing font-locking of unicode forall etc.Gravatar Pierre Courtieu2016-06-08
|
* Merge branch 'master' of github.com:ProofGeneral/PGGravatar Pierre Courtieu2016-05-27
|\
* | Fixing a smal glitch in indentation.Gravatar Pierre Courtieu2016-05-27
| |
| * Update license information for new logoGravatar Clément Pit--Claudel2016-05-25
| |
| * Update PG's logoGravatar Clément Pit--Claudel2016-05-24
|/ | | | | | | The new art is a contribution of Yoshihiro Imai (http://proofcafe.org/~yoshihiro503/), first released at https://github.com/yoshihiro503/generaltan and kindly made available under the terms of the GPL. Many thanks!
* Merge branch 'master' of github.com:ProofGeneral/PGGravatar Pierre Courtieu2016-05-20
|\
* | Fix #72+ make user keywords prioritized over default ones.Gravatar Pierre Courtieu2016-05-20
| |
| * Fail silently if Coq's version can't be detectedGravatar Clément Pit--Claudel2016-05-19
| | | | | | | | | | | | | | | | | | | | 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.
| * Merge branch 'master' of github.com:ProofGeneral/PGGravatar Clément Pit--Claudel2016-05-16
| |\ | |/ |/|
| * Don't offer "" as the default in C-c C-c C-aGravatar Clément Pit--Claudel2016-05-16
| |
| * coq-syntax: Add a debug specGravatar Clément Pit--Claudel2016-05-16
| |
* | Merge branch 'master' of github.com:ProofGeneral/PGGravatar Pierre Courtieu2016-05-02
|\|
* | Fixing detection of symbol at point.Gravatar Pierre Courtieu2016-05-02
| | | | | | | | | | | | Quote at start of a word should not be considered part of the word. Other characters than ' or _ are punctuation.
| * Don't use string-empty-pGravatar Clément Pit--Claudel2016-04-25
| | | | | | | | It's too recent
| * Merge pull request #68 from ProofGeneral/67-intros-and-PG-settingsGravatar Pierre Courtieu2016-04-15
|/| | | | | Respect user settings in coq-insert-intros
| * Respect user settings in coq-insert-introsGravatar Clément Pit--Claudel2016-04-14
|/ | | | Fixes #67.
* updating CHANGES to the last commit.Gravatar Pierre Courtieu2016-03-21
|
* Option to toggle optimising response windo heigth.Gravatar Pierre Courtieu2016-03-21
|
* Adding more keywords (Local xxx).Gravatar Pierre Courtieu2016-03-09
|
* Fixed #64 again. e2c5da0 commits was wrong.Gravatar Pierre Courtieu2016-03-09
|
* Fix #47.Gravatar Pierre Courtieu2016-03-09
| | | | There are many other issued with coq-smie-forward-token.
* Fix #64. Use syntax-ppss in fill-nobreak-predicate.Gravatar Pierre Courtieu2016-03-09
| | | | | More robust to font-lock tweaks that change font inside comments (whitespace mode etc).
* Fixing a small glitch in indentation.Gravatar Pierre Courtieu2016-03-09
| | | | | if a "; tactic" is not at the end of its line, (hanging) then it should not act on indetation of next line.
* Fix #63 (efficiency pb in indentation).Gravatar Pierre Courtieu2016-03-09
|
* Fixing #62.Gravatar Pierre Courtieu2016-03-08
| | | | | I don't know if it is a coq bug that bullet do not support Time. I remove Time from bullets for the moment.
* Avoiding useless computation in indentation code.Gravatar Pierre Courtieu2016-03-08
|
* Should fix #49 and #55 (compilation of From .. Require).Gravatar Pierre Courtieu2016-03-08
|
* Small fix for -Q options in loadpath.Gravatar Pierre Courtieu2016-03-08
|
* Highlight ltac:(), constr:(), and uconstr:()Gravatar Clément Pit--Claudel2016-03-05
| | | | Also refactor coq-font-lock-keywords-1 slightly.
* Redo 11b03d4 (ensure that ‘Time’ isn't added to internal commands)Gravatar Clément Pit--Claudel2016-02-29
|
* Remove leftover commentGravatar Clément Pit--Claudel2016-02-28
|
* Don't add the ‘Time’ prefix to internal Coq commandsGravatar Clément Pit--Claudel2016-02-28
| | | | | This ensures that parts of Proof General that use Coq commands in the background are not confused by extra timing information.
* Add uconstr to the (ltac constr) list in SMIEGravatar Clément Pit--Claudel2016-02-27
|
* Fix a typo: s/coq-modulestart-proofstart/coq-indent-proofstart/Gravatar Clément Pit--Claudel2016-02-27
|
* Add a :safe predicate to indentation variablesGravatar Clément Pit--Claudel2016-02-27
| | | | This is useful if people want to set them project-locally.
* Simplify code to add to .emacsGravatar Clément Pit--Claudel2016-02-20
|
* Adding missing keywordsGravatar Pierre Courtieu2016-02-18
|
* Merge pull request #28 from JasonGross/travis-24-3-4-5Gravatar Pierre Courtieu2016-02-17
|\ | | | | travis.yml for emacs 24.{3,4,5}
* \ Merge pull request #40 from hendriktews/proof-treeGravatar Pierre Courtieu2016-02-17
|\ \ | | | | | | basic proof tree changes for Coq 8.5
* | | More version number fixesGravatar Clément Pit--Claudel2016-02-13
| | |
* | | A few clarifications in READMEGravatar Clément Pit--Claudel2016-02-12
| | |
* | | Merge pull request #48 from tchajed/texi2html-flagsGravatar Clément Pit--Claudel2016-02-10
|\ \ \ | | | | | | | | Update numbering flag passed to texi2html
| * | | Update numbering flag passed to texi2htmlGravatar Tej Chajed2016-02-10
|/ / / | | | | | | | | | | | | | | | texi2html, as of version 1.80 (http://download-mirror.savannah.gnu.org/releases//texi2html/NEWS-1.80), uses -number-sections instead of -number for the flag name.
* | | More README updatesGravatar Clément Pit--Claudel2016-02-10
| | |
* | | Update READMEGravatar Clément Pit--Claudel2016-02-10
| | |
* | | Ensure that version detection does not fail in 24.3Gravatar Clément Pit--Claudel2016-02-06
| | |
* | | Use coq-prog-name to autodetect version numberGravatar Clément Pit--Claudel2016-02-06
| | |
* | | Fixed recent coq syntax change (tac !H become tac (H)).Gravatar Pierre Courtieu2016-01-27
| | |
| * | basic proof tree changes for Coq 8.5Gravatar Hendrik Tews2016-01-24
|/ / | | | | | | | | | | 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 23:32:57 +0000