aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
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
Also refactor coq-font-lock-keywords-1 slightly.
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
This ensures that parts of Proof General that use Coq commands in the background are not confused by extra timing information.
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
This is useful if people want to set them project-locally.
2016-02-20Simplify code to add to .emacsClément Pit--Claudel
2016-02-18Adding missing keywordsPierre Courtieu
2016-02-17Merge pull request #28 from JasonGross/travis-24-3-4-5Pierre Courtieu
travis.yml for emacs 24.{3,4,5}
2016-02-17Merge pull request #40 from hendriktews/proof-treePierre Courtieu
basic proof tree changes for Coq 8.5
2016-02-13More version number fixesClément Pit--Claudel
2016-02-12A few clarifications in READMEClément Pit--Claudel
2016-02-10Merge pull request #48 from tchajed/texi2html-flagsClément Pit--Claudel
Update numbering flag passed to texi2html
2016-02-10Update numbering flag passed to texi2htmlTej Chajed
texi2html, as of version 1.80 (http://download-mirror.savannah.gnu.org/releases//texi2html/NEWS-1.80), uses -number-sections instead of -number for the flag name.
2016-02-10More README updatesClément Pit--Claudel
2016-02-10Update READMEClément Pit--Claudel
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-02-03EasyCrypt mode: copyright + licensePierre-Yves Strub
2016-01-29Import EasyCrypt PG modePierre-Yves Strub
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
Fixes to get basic proof tree functionality, including support for give_up, cycle, swap, revgoals. Unshelve and evar's don't work yet, see proof-tree issues #1 and #2
2016-01-19Cleaning CHANGES.Pierre Courtieu
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-13Versions 24.2 and earlier do not compileJason Gross
2016-01-13Add .travis.yml file adapted from fstar-mode.elJason Gross
From https://github.com/FStarLang/fstar-mode.el/blob/master/.travis.yml
2016-01-08Fixing indentation of ";".Pierre Courtieu
Local/Global Tactic Notation
2016-01-08indentation of ";" more accurate.Pierre Courtieu
Now detecting if the ; is inside a parenthesized tactic (--> no spurious indentation).
2016-01-08Fixing outdenting in ";" indetation.Pierre Courtieu
2016-01-08Trying to indent ";" differently inside Ltac defs.Pierre Courtieu
This only works when the command starts with "Ltac". Ideally we would like to switch to no indentation of ";" each time the ";" is the child of something else that ends a command "." or bullets).
2016-01-07Fixed indentation of ";" tactical.Pierre Courtieu
2016-01-06Merge pull request #22 from ProofGeneral/fix-scrolling-buffersPierre Courtieu
Fix spurious scrolling of *goals* and *response* buffers
2016-01-06updating CHANGESPierre Courtieu
2016-01-06Adding uset preference coq-indent-semicolon-tactical.Pierre Courtieu
Some people prefer ";" tactical to be non indented, in particular in Ltac definitions. Setting this variable to 0 (2 by default) does it. You can still have some indentation by putting ; at beginning of lines: tac1 ; tac2 ; tac3.
2016-01-06Fixing #25.Pierre Courtieu
proof-script-buffer was not set before calling proof-shell-ready-prover.
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
Maybe need coq fix.
2015-12-31Fix spurious scrolling of *goals* and *response* buffersClément Pit--Claudel
See https://github.com/cpitclaudel/company-coq/issues/8 and https://github.com/cpitclaudel/company-coq/issues/32 for some background info.
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
Need some more refactoring actually: Some code from coq-compile-common became necessary to coq/pg globally. We shoudl refelct this by moving these parts somewhere else.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 13:10:57 +0000