aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
Commit message (Expand)AuthorAge
* 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
| * Respect user settings in coq-insert-introsGravatar Clément Pit--Claudel2016-04-14
|/
* 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
* Adding missing keywordsGravatar Pierre Courtieu2016-02-18
* Merge pull request #40 from hendriktews/proof-treeGravatar Pierre Courtieu2016-02-17
|\
* | 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
|/
* 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
* Automatically detect which version of Coq we're usingGravatar Clément Pit--Claudel2016-01-14
* Refactor the project file parsing codeGravatar Clément Pit--Claudel2016-01-14
* Fix #29 + indentation glitch + regexp refactoring.Gravatar Pierre Courtieu2016-01-14
* Fixing indentation of ";".Gravatar Pierre Courtieu2016-01-08
* indentation of ";" more accurate.Gravatar Pierre Courtieu2016-01-08
* Fixing outdenting in ";" indetation.Gravatar Pierre Courtieu2016-01-08
* Trying to indent ";" differently inside Ltac defs.Gravatar Pierre Courtieu2016-01-08
* Fixed indentation of ";" tactical.Gravatar Pierre Courtieu2016-01-07
* Merge pull request #22 from ProofGeneral/fix-scrolling-buffersGravatar Pierre Courtieu2016-01-06
|\
* | Adding uset preference coq-indent-semicolon-tactical.Gravatar Pierre Courtieu2016-01-06
* | Fixing #25.Gravatar Pierre Courtieu2016-01-06
* | Fixing #20. #19 fixed by a commit in coq-8.5.Gravatar Pierre Courtieu2016-01-06
* | First try to fix #19 and #20. Not finished.Gravatar Pierre Courtieu2016-01-04