aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2016-07-26Rename FAQ -> FAQ.mdErik Martin-Dorel
2016-07-23Add documentation about the recommended way to set coq-prog-name.Erik Martin-Dorel
2016-07-23Run "make magic" to update texi comments from elisp docstrings.Erik Martin-Dorel
2016-07-23Add myself to the list of maintainers.Erik Martin-Dorel
2016-07-22Adding 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-20Merge pull request #87 from erikmd/patch-1Pierre Courtieu
Fix (next-undo-elt) to return a relevant undo element w.r.t (undo-delta)
2016-07-07Fix inforef references to the emacs manual. (#88)Yuval Langer
2016-07-04Fix (next-undo-elt) to return a relevant undo element w.r.t (undo-delta).Erik Martin-Dorel
2016-07-03Highlight Existing Class like Existing Instance (#85)Jason Gross
Closes #81
2016-07-03Add Travis CI badge.Erik Martin-Dorel
2016-07-03emacs-git Travis build: Fix URL of Emacs repo & Build against emacs-25 branch.Erik Martin-Dorel
Ref: https://github.com/FStarLang/fstar-mode.el/blob/master/Makefile.travis
2016-07-03Update README.md.Erik Martin-Dorel
- Specify the language for code excerpts - Refactor the "More info" section.
2016-07-03Update a link (for latest version of FAQ).Erik Martin-Dorel
2016-07-03Fix link.Erik Martin-Dorel
2016-07-01Highlight [nra] like [nia] and [lia] and [lra] (#84)Jason Gross
2016-06-23Fix a typoClément Pit--Claudel
2016-06-23Add myself to list of authorsClément Pit--Claudel
2016-06-23par-compile: Don't try to compile plugins (cm.*)Clément Pit--Claudel
2016-06-23Fix a type error hidden until recent emacs.Pierre Courtieu
2016-06-23Updating CHANGES.Pierre Courtieu
2016-06-23Coq: option to prefer top over bottom of concl.Pierre Courtieu
2016-06-18coq-load-path docs: norec -> nonrec (#79)Timothy Bourke
2016-06-10Reset proof-script-buffer to nil if -ready-prover failsClément Pit--Claudel
Fixes #65
2016-06-10Color lia, romega, nia, psatz, nsatz, lraJason Gross
This closes #77
2016-06-08abbrev twivking.Pierre Courtieu
2016-06-08Fixing font-locking of unicode forall etc.Pierre Courtieu
2016-05-27Merge branch 'master' of github.com:ProofGeneral/PGPierre Courtieu
2016-05-27Fixing a smal glitch in indentation.Pierre Courtieu
2016-05-25Update license information for new logoClément Pit--Claudel
2016-05-24Update PG's logoClément Pit--Claudel
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!
2016-05-20Merge branch 'master' of github.com:ProofGeneral/PGPierre Courtieu
2016-05-20Fix #72+ make user keywords prioritized over default ones.Pierre Courtieu
2016-05-19Fail silently if Coq's version can't be detectedClé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-16Merge branch 'master' of github.com:ProofGeneral/PGClément Pit--Claudel
2016-05-16Don't offer "" as the default in C-c C-c C-aClément Pit--Claudel
2016-05-16coq-syntax: Add a debug specClément Pit--Claudel
2016-05-02Merge branch 'master' of github.com:ProofGeneral/PGPierre Courtieu
2016-05-02Fixing 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-25Don't use string-empty-pClément Pit--Claudel
It's too recent
2016-04-15Merge pull request #68 from ProofGeneral/67-intros-and-PG-settingsPierre Courtieu
Respect user settings in coq-insert-intros
2016-04-14Respect user settings in coq-insert-introsClément Pit--Claudel
Fixes #67.
2016-03-21updating CHANGES to the last commit.Pierre Courtieu
2016-03-21Option to toggle optimising response windo heigth.Pierre Courtieu
2016-03-09Adding more keywords (Local xxx).Pierre Courtieu
2016-03-09Fixed #64 again. e2c5da0 commits was wrong.Pierre Courtieu
2016-03-09Fix #47.Pierre Courtieu
There are many other issued with coq-smie-forward-token.
2016-03-09Fix #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-09Fixing 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-09Fix #63 (efficiency pb in indentation).Pierre Courtieu
2016-03-08Fixing #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.