aboutsummaryrefslogtreecommitdiff
path: root/coq/coq.el
AgeCommit message (Expand)Author
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-09Fixed #64 again. e2c5da0 commits was wrong.Pierre Courtieu
2016-03-09Fix #64. Use syntax-ppss in fill-nobreak-predicate.Pierre Courtieu
2016-03-08Fixing #62.Pierre Courtieu
2016-02-29Redo 11b03d4 (ensure that ‘Time’ isn't added to internal commands)Clément Pit--Claudel
2016-02-28Don't add the ‘Time’ prefix to internal Coq commandsClément Pit--Claudel
2016-02-17Merge pull request #40 from hendriktews/proof-treePierre Courtieu
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-06Merge pull request #22 from ProofGeneral/fix-scrolling-buffersPierre 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-10Fixing variable declaration.Pierre Courtieu
2015-12-09Adding an setting for Search Blacklist coq option.Pierre Courtieu
2015-12-04Fixed a typo.Pierre Courtieu
2015-11-26A shortcut for coq-insert-as-in-next-command.Pierre Courtieu
2015-11-13Experimenting less brutal frame deletion.Pierre Courtieu
2015-11-13Fixed auto-width setting not initialized (trac #456).Pierre Courtieu
2015-11-13Cleaning code for auto width adapting.Pierre Courtieu
2015-11-12Tentative fix for #10Clément Pit--Claudel
2015-11-12Debuging: display a warning.Pierre Courtieu
2015-11-02coq-pre-v85 option to fix coqdep invocation in [compile before require].Pierre Courtieu
2015-10-20Re-thinking auto-insert-as.Pierre Courtieu
2015-10-13Fixed coq-id-at-point.Pierre Courtieu
2015-10-13proof-retract-command-hook added + more auto adjust width in coq mode.Pierre Courtieu
2015-10-12proof-assert-command-hook added + Auto adjust width in coq mode.Pierre Courtieu
2015-10-09Fixing < 25 use of window-frame (mandatory arg).Pierre Courtieu
2015-10-06Put 'delete-selection t on coq-terminator-insertClément Pit--Claudel
2015-10-06Trying to deal with debug mode.Pierre Courtieu
2015-09-29Fixed #1 (Missing space in coq-insert-intros).Pierre Courtieu
2015-09-25More Fixes when issuing commands from another buffer.Pierre Courtieu
2015-09-25Fixed bug when issuing commands from another buffer than scripting one.Pierre Courtieu
2015-06-23Added a moderate support for double quotes in -arg lines of _CoqProject.Pierre Courtieu
2015-05-19robustify last commit (disabling smie show-paren).Pierre Courtieu
2015-05-19Disable smie parenthesis blink. Too slow sometimes.Pierre Courtieu
2015-05-07Fixes #485.Pierre Courtieu
2015-04-27Fixed at-point detection (bis).Pierre Courtieu
2015-04-27Fixed at-point detection.Pierre Courtieu
2015-04-14bold unicode biders + Fixing highlighting in goals and response buffers + cle...Pierre Courtieu
2015-04-02Highlighting stuff in goals mode (C-c C-a C-h). Very basic for now.Pierre Courtieu
2015-04-01Fix fill-paragraph merging comments and code (never fill code).Pierre Courtieu