aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Bump version from 4.4.1~pre to 4.5-gitGravatar Erik Martin-Dorel2018-08-22
| | | | This commit ensures the version number is (version-to-list)-compliant.
* Set the minimal supported version of emacs to 24.3 instead of 24.4Gravatar Erik Martin-Dorel2018-08-22
| | | | | | | | This agrees with the minimal version of GNU Emacs currently tested by Travis CI, as well as with the version packaged in Ubuntu 14.04 LTS Reference: https://github.com/ProofGeneral/PG/issues/368#issuecomment-397561986
* Merge pull request #200 from craff/masterGravatar Erik Martin-Dorel2018-08-22
|\ | | | | Update phox support
* \ Merge pull request #379 from tchajed/variant-keywordGravatar Clément Pit-Claudel2018-08-21
|\ \ | | | | | | Support the Variant vernacular
* \ \ Merge branch 'master' of github.com:ProofGeneral/PGGravatar Pierre Courtieu2018-08-18
|\ \ \
* | | | Fix #7980, keep option order unchanged.Gravatar Pierre Courtieu2018-08-18
| | | |
| | * | Support the Variant vernacularGravatar Tej Chajed2018-08-17
| |/ / | | | | | | | | | | | | Syntactically looks much like an Inductive, though it is non-recursive so "where" (mutual recursion) is not supported.
| * | Merge pull request #378 from user454322/patch-1Gravatar Clément Pit-Claudel2018-08-15
| |\ \ | | | | | | | | Fix typo in INSTALL file
| | * | Update INSTALLGravatar Javier2018-08-15
| |/ /
| * | Merge pull request #375 from jmgrosen/masterGravatar Clément Pit-Claudel2018-08-07
|/| | | | | | | | Add coq-Print-Ltac to print an Ltac term
| * | Add coq-Print-Ltac to print an Ltac termGravatar John Grosen2018-08-07
|/ /
* | Fixing last commit.Gravatar Pierre Courtieu2018-06-15
| |
* | Fix #368 (emacs < 25 split-string has no trim arg).Gravatar Pierre Courtieu2018-06-15
| | | | | | | | Copied some code from company-coq.
* | small fix on hyp overlays.Gravatar Pierre Courtieu2018-06-13
| |
* | Fix multiple hyp overlays.Gravatar Pierre Courtieu2018-06-13
| | | | | | | | | | queries would trigger re-generarion of overlays. Now overlays are generated if there are no overlays already.
* | Fix the fix #355.Gravatar Pierre Courtieu2018-06-13
| | | | | | | | The fix was bad: no ore hyps were foldable/highlightable.
* | Small bug unhighlighting.Gravatar Pierre Courtieu2018-06-11
| | | | | | | | | | Selecting the unhighlightied hyps showed a different region color. Setting the face to nil is better.
* | fix #355 + probable bug.Gravatar Pierre Courtieu2018-06-11
| | | | | | | | | | By renaming the arg load-path into loadpath I notice that a coq-load-path was used instead of it.
* | key maps + small glitch hyp highlight/folding code.Gravatar Pierre Courtieu2018-06-11
| |
* | Changed the look of folding/unfolding hyps.Gravatar Pierre Courtieu2018-06-08
| |
* | Small fix in a regexp.Gravatar Pierre Courtieu2018-06-06
| |
* | Shorter CHANGES + smal fixes in hide/highlight hyps code.Gravatar Pierre Courtieu2018-06-04
| |
* | Click hypothesis to (un)hide them.Gravatar Pierre Courtieu2018-06-01
| |
* | Fixed a typo in previous commits.Gravatar Pierre Courtieu2018-06-01
| |
* | Updated CHANGES about hiding and highlighting of hyps.Gravatar Pierre Courtieu2018-05-31
| |
* | Infrastructure for hypothesis hiding.Gravatar Pierre Courtieu2018-05-31
| |
* | Fixing infrastructure for hypothesis highlighting.Gravatar Pierre Courtieu2018-05-31
| |
* | Merge branch 'master' of github.com:ProofGeneral/PGGravatar Pierre Courtieu2018-05-31
|\ \
* | | Infrastructure for transient hyps highlighting.Gravatar Pierre Courtieu2018-05-31
| | |
| * | Merge pull request #360 from ProofGeneral/update-readmeGravatar Erik Martin-Dorel2018-05-29
| |\ \ | | | | | | | | Update README.md (about PG branches and license)
| | * | Add note about PG branches and licenseGravatar Erik Martin-Dorel2018-05-29
| |/ /
| * | Merge pull request #356 from stardiviner/stardiviner-patch-1Gravatar Erik Martin-Dorel2018-04-22
| |\ \ | | | | | | | | Fix coq-symbol-face's :inherit attribute
| | * | small fix of face `coq-symbol-face'Gravatar stardiviner2018-04-22
| |/ /
| * | Merge pull request #207 from SkySkimmer/masterGravatar Erik Martin-Dorel2018-04-08
| |\ \ | | | | | | | | Make coq-prog-args safe when list of strings.
| * | | Merge pull request #347 from liyishuai/masterGravatar Erik Martin-Dorel2018-03-17
|/| | | | | | | | | | | Setup CI for Emacs 25.3
| * | | CI Emacs 25.3Gravatar Yishuai Li2018-03-11
|/ / /
* | | Merge pull request #344 from ProofGeneral/font-lock-fixGravatar Erik Martin-Dorel2018-03-07
|\ \ \ | | | | | | | | Add a missing parameter in advice on font-lock-fontify-keywords-region
| * | | Add a missing parameter in advice on font-lock-fontify-keywords-regionGravatar Clément Pit--Claudel2018-03-07
|/ / /
* | | Fix typos in custom variable descriptions. (#236)Gravatar Tej Chajed2018-03-03
| | |
* | | Update the AUTHORS file.Gravatar Erik Martin-Dorel2018-03-03
| | |
* | | Merge pull request #194 from ProofGeneral/update-headersGravatar Clément Pit-Claudel2018-02-25
|\ \ \ | | | | | | | | Update copyright messages and improve the header of elisp files.
| * | | Update copyright messages and improve the header of elisp files.Gravatar Erik Martin-Dorel2018-02-21
|/ / /
* | | Bind C-c C-m (= C-c RET) to proof-goto-point [tty] (#228)Gravatar Erik Martin-Dorel2018-02-20
| | | | | | | | | Close ProofGeneral/PG#31
* | | typo in abbrevs.Gravatar Pierre Courtieu2018-02-07
| | |
* | | Merge pull request #224 from psteckler/fix-233Gravatar Pierre Courtieu2018-01-30
|\ \ \ | | | | | | | | Look for vernac controls before focus bracket, possible fix for #223
| * | | look for vernac controls before focus bracket, fix for #223Gravatar Paul Steckler2018-01-26
|/ / /
* | | Disable ASLR during Travis buildsGravatar Clément Pit--Claudel2018-01-17
| | |
* | | Get rid of old-style backquotesGravatar Clément Pit--Claudel2018-01-16
| | | | | | | | | | | | Closes #221. Thanks @jwiegley!
* | | Experimental fix for #220.Gravatar Pierre Courtieu2018-01-15
| | |
| * | Make coq-prog-args safe when list of strings.Gravatar Gaëtan Gilbert2017-12-22
| | | | | | | | | | | | They could be passed through _CoqProject regardless.