aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Update license information for new logoGravatar Clément Pit--Claudel2016-05-25
* Update PG's logoGravatar Clément Pit--Claudel2016-05-24
* 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
| * 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
| * Don't use string-empty-pGravatar Clément Pit--Claudel2016-04-25
| * Merge pull request #68 from ProofGeneral/67-intros-and-PG-settingsGravatar Pierre Courtieu2016-04-15
|/|
| * Respect user settings in coq-insert-introsGravatar Clément Pit--Claudel2016-04-14
|/
* 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
* Fix #64. Use syntax-ppss in fill-nobreak-predicate.Gravatar Pierre Courtieu2016-03-09
* Fixing a small glitch in indentation.Gravatar Pierre Courtieu2016-03-09
* Fix #63 (efficiency pb in indentation).Gravatar Pierre Courtieu2016-03-09
* Fixing #62.Gravatar Pierre Courtieu2016-03-08
* 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
* 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
* 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
* 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
|\
* \ Merge pull request #40 from hendriktews/proof-treeGravatar Pierre Courtieu2016-02-17
|\ \
* | | 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 texi2htmlGravatar Tej Chajed2016-02-10
|/ / /
* | | 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
|/ /
* | Cleaning CHANGES.Gravatar Pierre Courtieu2016-01-19
* | fix #36.Gravatar Pierre Courtieu2016-01-19
* | Add a few comments to explain values of coq-load-pathGravatar Clément Pit--Claudel2016-01-14
* | Mark coq-load-path-include-current as obsoleteGravatar Clément Pit--Claudel2016-01-14