aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Make shell and perl scripts executable.Gravatar Erik Martin-Dorel2016-09-19
| | | | This addresses part of the issues pointed out in #112
* Bump version number for next release cycle.Gravatar Erik Martin-Dorel2016-09-19
|
* Update the documentation and prepare the release 4.4.Gravatar Erik Martin-Dorel2016-09-18
|
* Comment-out the rcsid ($Id$) that dates from CVS.Gravatar Erik Martin-Dorel2016-09-18
|
* Detail.Gravatar Erik Martin-Dorel2016-09-18
|
* Promote CHANGES since 2820cb68 as related to PG 4.4.Gravatar Erik Martin-Dorel2016-09-18
|
* Fix reference to log-warning-minimum-levelGravatar psteckler2016-09-16
| | | Fixes #110.
* Ensure PG overlays have pg-span property (#98)Gravatar Tej Chajed2016-08-25
|
* Sort the OPTIONS menu items differently & Fix a typo (UnSet -> Unset).Gravatar Erik Martin-Dorel2016-08-14
|
* Replace "Set Implicit Arguments" option with "Set Printing Implicit".Gravatar Erik Martin-Dorel2016-08-14
| | | | Closes #99.
* Add Reserved Infix like Reserved Notation (#95)Gravatar Jason Gross2016-08-14
|
* Fix whitespace to comply with Markdown syntax.Gravatar Erik Martin-Dorel2016-07-26
|
* Rename FAQ -> FAQ.mdGravatar Erik Martin-Dorel2016-07-26
|
* Add documentation about the recommended way to set coq-prog-name.Gravatar Erik Martin-Dorel2016-07-23
|
* Run "make magic" to update texi comments from elisp docstrings.Gravatar Erik Martin-Dorel2016-07-23
|
* Add myself to the list of maintainers.Gravatar Erik Martin-Dorel2016-07-23
|
* 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.
* Merge pull request #87 from erikmd/patch-1Gravatar Pierre Courtieu2016-07-20
|\ | | | | Fix (next-undo-elt) to return a relevant undo element w.r.t (undo-delta)
* | Fix inforef references to the emacs manual. (#88)Gravatar Yuval Langer2016-07-07
| |
| * Fix (next-undo-elt) to return a relevant undo element w.r.t (undo-delta).Gravatar Erik Martin-Dorel2016-07-04
|/
* Highlight Existing Class like Existing Instance (#85)Gravatar Jason Gross2016-07-03
| | | Closes #81
* Add Travis CI badge.Gravatar Erik Martin-Dorel2016-07-03
|
* emacs-git Travis build: Fix URL of Emacs repo & Build against emacs-25 branch.Gravatar Erik Martin-Dorel2016-07-03
| | | | Ref: https://github.com/FStarLang/fstar-mode.el/blob/master/Makefile.travis
* Update README.md.Gravatar Erik Martin-Dorel2016-07-03
| | | | | - Specify the language for code excerpts - Refactor the "More info" section.
* Update a link (for latest version of FAQ).Gravatar Erik Martin-Dorel2016-07-03
|
* Fix link.Gravatar Erik Martin-Dorel2016-07-03
|
* Highlight [nra] like [nia] and [lia] and [lra] (#84)Gravatar Jason Gross2016-07-01
|
* Fix a typoGravatar Clément Pit--Claudel2016-06-23
|
* Add myself to list of authorsGravatar Clément Pit--Claudel2016-06-23
|
* par-compile: Don't try to compile plugins (cm.*)Gravatar Clément Pit--Claudel2016-06-23
|
* Fix a type error hidden until recent emacs.Gravatar Pierre Courtieu2016-06-23
|
* Updating CHANGES.Gravatar Pierre Courtieu2016-06-23
|
* Coq: option to prefer top over bottom of concl.Gravatar Pierre Courtieu2016-06-23
|
* coq-load-path docs: norec -> nonrec (#79)Gravatar Timothy Bourke2016-06-18
|
* Reset proof-script-buffer to nil if -ready-prover failsGravatar Clément Pit--Claudel2016-06-10
| | | | Fixes #65
* Color lia, romega, nia, psatz, nsatz, lraGravatar Jason Gross2016-06-10
| | | | This closes #77
* 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.