| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-12-13 | Use `cl-lib` instead of `cl` everywhere | Stefan Monnier | |
| Use lexical-binding in a few files where it was easy. Don't require `proof-compat` when it's not used. * coq/coq-db.el: Use lexical-binding. * coq/coq-system.el: Use lexical-binding. (coq--extract-prog-args): Use concatenated-args rather than recomputing it. * coq/coq.el: Require `span` to silence some warnings. * generic/pg-user.el: Use lexical-binding. (complete, add-completion, completion-min-length): Silence warnings. * generic/pg-xml.el: Use lexical-binding. (pg-xml-string-of): Prefer mapconcat to reduce+concat. * generic/proof-depends.el: Use lexical-binding. (proof-dep-split-deps): Use `push`. * generic/proof-shell.el: Require `span` to silence some warnings. (proof-shell-invisible-command): Don't use lexical-let just to build a wasteful η-redex! * lib/holes.el: Use lexical-binding. Remove redundant :group args. * lib/span.el: Use lexical-binding. (span-read-only-hook): Use user-error. (span-raise): Remove, unused. | |||
| 2018-08-23 | Fix most doc issues raised by (checkdoc) | Erik Martin-Dorel | |
| 2018-02-21 | Update copyright messages and improve the header of elisp files. | Erik Martin-Dorel | |
| 2017-05-24 | Remove mmm and ML4PG contribs and remove references to them in code and docs | Paul Steckler | |
| 2017-03-08 | Fix incorrect uses of defvar | Clément Pit--Claudel | |
| It didn't really matter that these variables were defined and set to nil during compilation, since we ran compilation in a clean Emacs in --batch mode; it does matter now, however, since package.el compiles PG in the user's currently running Emacs instance. | |||
| 2015-03-13 | (fixes last commit) Added a command to send Queries to coq, with completion ↵ | Pierre Courtieu | |
| (C-c C-a C-q). Should replace C-c C-v at some point. Needs to have a complete list of such queries. Obeys C-u prefix for Printing all flag. | |||
| 2012-09-19 | Small fix in holes code. | Pierre Courtieu | |
| 2012-08-30 | Summary: Don't quote lambda expressions | Stefan Monnier | |
| * coq/coq-indent.el (coq-indent-inner-regexp): Remove old X-Symbol element. (coq-save-count, coq-proof-count): * obsolete/plastic/plastic.el (plastic-shell-handle-output): * lib/texi-docstring-magic.el (texi-docstring-magic-insert-magic): * lib/pg-dev.el (emacs-lisp-mode-hook): * lib/maths-menu.el (maths-menu-filter-predicate) (maths-menu-tokenise-insert): * lib/holes.el (holes-next): * lego/lego.el (lego-shell-handle-output): * isar/isabelle-system.el (isabelle-docs-menu): * coq/coq.el (coq-compile-command, coq-compile-auto-save) (coq-compile-ignored-directories, coq-load-path-safep) (proof-shell-handle-delayed-output-hook): Don't quote lambda. | |||
| 2009-09-06 | Rearrange for scoping | David Aspinall | |
| 2009-09-06 | Add menu moved from Coq menu. Make deactivating holes-mode forget all holes. | David Aspinall | |
| 2009-09-06 | Make holes-abbrev-complete obey status of minor mode. | David Aspinall | |
| 2009-09-06 | Cleanup code and use define-minor-mode. | David Aspinall | |
| 2009-09-05 | Tidy whitespace | David Aspinall | |
| 2009-01-14 | Made indentation optional when replaing # by holes. | Pierre Courtieu | |
| 2008-10-22 | Fixing parenthesis not accepted by recent emacs anymore. fix by Stefan | Pierre Courtieu | |
| Monnier. | |||
| 2008-07-24 | Merge changes from Version4Branch. | David Aspinall | |
| 2008-07-21 | Changed the main menu of coq. Changed a shortcut for holes. | Pierre Courtieu | |
| 2008-01-30 | Fix RCS tags | David Aspinall | |
| 2008-01-28 | Don't give error when loaded during "make doc" with old emacs version | David Aspinall | |
| 2008-01-15 | Many compatibility updates, bug fixes, rearrangements for compilation. | David Aspinall | |
| 2008-01-03 | Fixed abbrev installation. + small fixes. | Pierre Courtieu | |
| 2007-12-13 | holes-skeleton-end-hook: no action if mmm-inside-insert-by-key bound | David Aspinall | |
| 2006-08-21 | Started the coq-insert-tactic. | Pierre Courtieu | |
| 2006-01-10 | commit of a small patch from Stefan Monnier, to fix a small bug of | Pierre Courtieu | |
| drag-mouse-region with holes. | |||
| 2005-03-10 | debugging and cleaning of holes.el. | Pierre Courtieu | |
| 2005-03-08 | small modifications, updating doc string of holes.el. | Pierre Courtieu | |
| 2005-03-08 | making holes.el cleaner, with the help of Stefan Monnier. I had to | Pierre Courtieu | |
| adapt coq.el to these modifications. | |||
| 2005-03-01 | cleaning holes.el, starting to making it compatible with skeletons. | Pierre Courtieu | |
| 2005-03-01 | debugging of holes.el. | Pierre Courtieu | |
| 2005-02-21 | Debugging holes.el, starting trying to use skeletons. | Pierre Courtieu | |
| 2005-02-21 | Cleaning file holes.el (tab-width, docstring etc). | Pierre Courtieu | |
| 2005-02-17 | Updated the doc for new pg/coq. Made modifications advised by Stefan | Pierre Courtieu | |
| Monnier on holes.el. | |||
| 2005-02-16 | debugging the new holes-mode for fsf emacs. Keyboard shortcuts was | Pierre Courtieu | |
| badly defined. | |||
| 2005-02-15 | Modified holes doc string to fit to new shortcut of holes-mode. | Pierre Courtieu | |
| 2005-02-15 | Finished making holes.el a real minor-mode. There is a new file | Pierre Courtieu | |
| holes-load.el which defines the autoloads (enough of them?). All functions have the prefix "holes-", and offending keyboard shortcuts have been either removed or bound to the minor mode. I made holes-mode minor mode automatically turned on in all proof buffers in coq mode (including shell, script and response buffers as it may be useful to copy paste parts of this buffers into holes). | |||
| 2005-02-14 | cleaning holes.el. All functions are prefixed with "holes-". Also | Pierre Courtieu | |
| modified coq.el and coq-abbrev.el accordingly. | |||
| 2005-02-14 | Starting to clean holes.el following Stefan Monnier's advices. Making | Pierre Courtieu | |
| holes a real minor-mode. | |||
| 2004-08-25 | Renamed file | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |