aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Merge pull request #396 from dbp/coqproject-localGravatar Clément Pit-Claudel2018-10-30
|\ | | | | Use non-remote path to expand paths in _CoqProject when file is remote.
| * Use non-remote path to expand paths in _CoqProject when file is remote.Gravatar Daniel Patterson2018-10-30
|/ | | | | | | | | When editing a remote file, the `coqtop` process will itself be remote, which means that the paths that are passed to it should be _local_, not remote. Otherwise, paths like '/ssh:hostname:/path/to/dir' get passed to `coqtop`, which has no idea what's going on. This relates to #203.
* Merge pull request #393 from anton-trunov/fix-coqproject-argGravatar Clément Pit-Claudel2018-09-27
|\ | | | | Fix parsing of -arg in _CoqProject file
| * Fix parsing of -arg in _CoqProject fileGravatar Anton Trunov2018-09-27
|/ | | | | The result of parsing was in reverse, see https://github.com/ProofGeneral/PG/issues/392\#issuecomment-425227314
* Reloading proof-autoloads is safe; don't forbid itGravatar Clément Pit-Claudel2018-09-01
| | | | | | Fixes GH-386. Reported-by: @mrkkrp
* Merge pull request #384 from ProofGeneral/update-install-guideGravatar Erik Martin-Dorel2018-08-30
|\ | | | | Update installation instructions for MELPA in README.md
| * Add MELPA badgeGravatar Erik Martin-Dorel2018-08-30
| |
| * Update the section of supported PAsGravatar Erik Martin-Dorel2018-08-30
| |
| * README.md: Update installation instructionsGravatar Erik Martin-Dorel2018-08-30
|/
* Merge pull request #169 from ProofGeneral/help-span-extendedGravatar Erik Martin-Dorel2018-08-25
|\ | | | | Fix #158 by extending helpspan
* | ProofGeneral.texi: Add EasyCrypt in the introGravatar Erik Martin-Dorel2018-08-23
| |
* | Update AUTHORS file for EasyCryptGravatar Erik Martin-Dorel2018-08-23
| |
* | Merge pull request #380 from ProofGeneral/prepare-melpaGravatar Erik Martin-Dorel2018-08-23
|\ \ | | | | | | Prepare PG for MELPA
| * | Run make autoloadsGravatar Erik Martin-Dorel2018-08-23
| | |
| * | Update AUTHORS, fixing 2 typosGravatar Erik Martin-Dorel2018-08-23
| | |
| * | Add link to the latex-pretty-symbols package mentioned by @craffGravatar Erik Martin-Dorel2018-08-23
| | | | | | | | | | | | Fix the typo reported by @siddharthist as well
| * | Fix most doc issues raised by (checkdoc)Gravatar Erik Martin-Dorel2018-08-23
| | |
| * | pg-init.el: Add metadata asked by (package-lint-current-buffer)Gravatar Erik Martin-Dorel2018-08-23
| | |
| * | Update Info dir file (so there’s no unwanted line break)Gravatar Erik Martin-Dorel2018-08-23
| | |
| * | 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
| |/ / /