aboutsummaryrefslogtreecommitdiff
path: root/coq
AgeCommit message (Expand)Author
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
2016-01-19fix #36.Pierre Courtieu
2016-01-14Add a few comments to explain values of coq-load-pathClément Pit--Claudel
2016-01-14Mark coq-load-path-include-current as obsoleteClément Pit--Claudel
2016-01-14Automatically detect which version of Coq we're usingClément Pit--Claudel
2016-01-14Refactor the project file parsing codeClément Pit--Claudel
2016-01-14Fix #29 + indentation glitch + regexp refactoring.Pierre Courtieu
2016-01-08Fixing indentation of ";".Pierre Courtieu
2016-01-08indentation of ";" more accurate.Pierre Courtieu
2016-01-08Fixing outdenting in ";" indetation.Pierre Courtieu
2016-01-08Trying to indent ";" differently inside Ltac defs.Pierre Courtieu
2016-01-07Fixed indentation of ";" tactical.Pierre Courtieu
2016-01-06Merge pull request #22 from ProofGeneral/fix-scrolling-buffersPierre Courtieu
2016-01-06Adding uset preference coq-indent-semicolon-tactical.Pierre Courtieu
2016-01-06Fixing #25.Pierre Courtieu
2016-01-06Fixing #20. #19 fixed by a commit in coq-8.5.Pierre Courtieu
2016-01-04First try to fix #19 and #20. Not finished.Pierre Courtieu
2015-12-31Fix spurious scrolling of *goals* and *response* buffersClément Pit--Claudel
2015-12-31comment and readme.Pierre Courtieu
2015-12-14Refactoring. New file coq-system.el.Pierre Courtieu
2015-12-14Small refactoring of coqxxx args detection.Pierre Courtieu
2015-12-14Fixing coq-prog-arg for auto compilation.Pierre Courtieu
2015-12-10Fixing variable declaration.Pierre Courtieu
2015-12-09Adding an setting for Search Blacklist coq option.Pierre Courtieu
2015-12-07Speeding up indentation (regexp optim).Pierre Courtieu
2015-12-07Speeding up indentation.Pierre Courtieu
2015-12-05Fixed #15 + more speedup of indentation.Pierre Courtieu
2015-12-04Fixed a typo.Pierre Courtieu
2015-11-30Speeding up indentation code (smie lexer).Pierre Courtieu
2015-11-26A shortcut for coq-insert-as-in-next-command.Pierre Courtieu
2015-11-23Introduce a coq-question-mark-faceClément Pit--Claudel
2015-11-17recompilation: Improve error checkingClément Pit--Claudel
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 01:43:10 +0000