aboutsummaryrefslogtreecommitdiff
path: root/coq
AgeCommit message (Expand)Author
2016-09-28Make it possible to work around #113Clément Pit--Claudel
2016-09-19Make shell and perl scripts executable.Erik Martin-Dorel
2016-08-14Sort the OPTIONS menu items differently & Fix a typo (UnSet -> Unset).Erik Martin-Dorel
2016-08-14Replace "Set Implicit Arguments" option with "Set Printing Implicit".Erik Martin-Dorel
2016-08-14Add Reserved Infix like Reserved Notation (#95)Jason Gross
2016-07-22Adding the option to highlight susual symbols.Pierre Courtieu
2016-07-03Highlight Existing Class like Existing Instance (#85)Jason Gross
2016-07-01Highlight [nra] like [nia] and [lia] and [lra] (#84)Jason Gross
2016-06-23Fix a typoClément Pit--Claudel
2016-06-23par-compile: Don't try to compile plugins (cm.*)Clément Pit--Claudel
2016-06-23Fix a type error hidden until recent emacs.Pierre Courtieu
2016-06-23Coq: option to prefer top over bottom of concl.Pierre Courtieu
2016-06-10Color lia, romega, nia, psatz, nsatz, lraJason Gross
2016-06-08abbrev twivking.Pierre Courtieu
2016-06-08Fixing font-locking of unicode forall etc.Pierre Courtieu
2016-05-27Fixing a smal glitch in indentation.Pierre Courtieu
2016-05-20Merge branch 'master' of github.com:ProofGeneral/PGPierre Courtieu
2016-05-20Fix #72+ make user keywords prioritized over default ones.Pierre Courtieu
2016-05-19Fail silently if Coq's version can't be detectedClément Pit--Claudel
2016-05-16Merge branch 'master' of github.com:ProofGeneral/PGClément Pit--Claudel
2016-05-16Don't offer "" as the default in C-c C-c C-aClément Pit--Claudel
2016-05-16coq-syntax: Add a debug specClément Pit--Claudel
2016-05-02Merge branch 'master' of github.com:ProofGeneral/PGPierre Courtieu
2016-05-02Fixing detection of symbol at point.Pierre Courtieu
2016-04-25Don't use string-empty-pClément Pit--Claudel
2016-04-14Respect user settings in coq-insert-introsClément Pit--Claudel
2016-03-21Option to toggle optimising response windo heigth.Pierre Courtieu
2016-03-09Adding more keywords (Local xxx).Pierre Courtieu
2016-03-09Fixed #64 again. e2c5da0 commits was wrong.Pierre Courtieu
2016-03-09Fix #47.Pierre Courtieu
2016-03-09Fix #64. Use syntax-ppss in fill-nobreak-predicate.Pierre Courtieu
2016-03-09Fixing a small glitch in indentation.Pierre Courtieu
2016-03-09Fix #63 (efficiency pb in indentation).Pierre Courtieu
2016-03-08Fixing #62.Pierre Courtieu
2016-03-08Avoiding useless computation in indentation code.Pierre Courtieu
2016-03-08Should fix #49 and #55 (compilation of From .. Require).Pierre Courtieu
2016-03-08Small fix for -Q options in loadpath.Pierre Courtieu
2016-03-05Highlight ltac:(), constr:(), and uconstr:()Clément Pit--Claudel
2016-02-29Redo 11b03d4 (ensure that ‘Time’ isn't added to internal commands)Clément Pit--Claudel
2016-02-28Remove leftover commentClément Pit--Claudel
2016-02-28Don't add the ‘Time’ prefix to internal Coq commandsClément Pit--Claudel
2016-02-27Add uconstr to the (ltac constr) list in SMIEClément Pit--Claudel
2016-02-27Fix a typo: s/coq-modulestart-proofstart/coq-indent-proofstart/Clément Pit--Claudel
2016-02-27Add a :safe predicate to indentation variablesClément Pit--Claudel
2016-02-18Adding missing keywordsPierre Courtieu
2016-02-17Merge pull request #40 from hendriktews/proof-treePierre Courtieu
2016-02-06Ensure that version detection does not fail in 24.3Clément Pit--Claudel
2016-02-06Use coq-prog-name to autodetect version numberClément Pit--Claudel
2016-01-27Fixed recent coq syntax change (tac !H become tac (H)).Pierre Courtieu
2016-01-24basic proof tree changes for Coq 8.5Hendrik Tews
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 11:18:20 +0000