| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fix menu path to Customize |  David Aspinall | 2005-05-17 |
| | | |||
| * | Set version tag for new release. | David Aspinall | 2005-05-17 |
| | | |||
| * | - Don't just reuse visible frames but also iconified ones. | David Aspinall | 2005-05-17 |
| | | | | | | | - When proof-three-window-enable is nil, don't mark a dedicated window as non-dedicated. - Don't make the window-size-fixed. It's a real pain in the rear. | ||
| * | Documentation. | David Aspinall | 2005-05-17 |
| | | |||
| * | Disable Twelf support by default | David Aspinall | 2005-05-17 |
| | | |||
| * | Fix the removal of ".UTF-8" from LANG. | David Aspinall | 2005-05-17 |
| | | |||
| * | Updated. | David Aspinall | 2005-05-17 |
| | | |||
| * | Add missing lib/ | David Aspinall | 2005-05-17 |
| | | |||
| * | - shell-command-to-string can fail in various corner cases. | David Aspinall | 2005-05-17 |
| | | |||
| * | - Remove wrong docstring on make-detached-span. | David Aspinall | 2005-05-17 |
| | | | | | | | | - Basically rewrite span-overlay.el to better use the built-in overlay facilities. - Complain about the namespace pollution in span*.el. | ||
| * | Deleted file | David Aspinall | 2005-05-17 |
| | | |||
| * | Updated. | David Aspinall | 2005-05-17 |
| | | |||
| * | added -L option; |  Makarius Wenzel | 2005-05-17 |
| | | | | | tuned; | ||
| * | undeleted; | Makarius Wenzel | 2005-05-10 |
| | | |||
| * | Add FAQ about favourites | David Aspinall | 2005-04-27 |
| | | |||
| * | added some entris in coq menus. |  Pierre Courtieu | 2005-04-21 |
| | | |||
| * | cleaned a bit coq.el (checkdoc). Put some comments to tell what is to | Pierre Courtieu | 2005-04-20 |
| | | | | | be removed when coq-8.0 becomes unsupported. | ||
| * | New backtracking system for coq continues, this time it uses a new Coq | Pierre Courtieu | 2005-04-20 |
| | | | | | | | | | | | | | | | | | | command "Bactrack n m p", where n is the global state label to reach backward, p is the number of aborts and m is an absolute reference to the proof stack to undo (it is the proof stack depth). Coq prompt is now like this: state proof stack num depth __ _ aux < 12 |aux|SmallStepAntiReflexive| 4 < รน ^^^^^^ ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ ^ usual pending proofs usual special char See comments in coq-fin-and-forget-v81. | ||
| * | Updated. | David Aspinall | 2005-03-25 |
| | | |||
| * | New files. | David Aspinall | 2005-03-25 |
| | | |||
| * | Set version tag for new release. | David Aspinall | 2005-03-25 |
| | | |||
| * | Updated. | David Aspinall | 2005-03-25 |
| | | |||
| * | Remove project todos | David Aspinall | 2005-03-25 |
| | | |||
| * | Remove junk | David Aspinall | 2005-03-25 |
| | | |||
| * | Deleted file | David Aspinall | 2005-03-23 |
| | | |||
| * | Use another symbol | David Aspinall | 2005-03-23 |
| | | |||
| * | Changes from Clemens Ballarin for large X-Symbol fonts | David Aspinall | 2005-03-23 |
| | | |||
| * | New files. | David Aspinall | 2005-03-23 |
| | | |||
| * | Large fonts | David Aspinall | 2005-03-23 |
| | | |||
| * | Updated. | David Aspinall | 2005-03-21 |
| | | |||
| * | Mention Stefan's patches | David Aspinall | 2005-03-21 |
| | | |||
| * | debugging and cleaning of holes.el. | Pierre Courtieu | 2005-03-10 |
| | | |||
| * | 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 | 2005-03-08 |
| | | | | | adapt coq.el to these modifications. | ||
| * | cleaning holes.el, starting to making it compatible with skeletons. | Pierre Courtieu | 2005-03-01 |
| | | |||
| * | debugging of holes.el. | Pierre Courtieu | 2005-03-01 |
| | | |||
| * | 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-21 |
| | | |||
| * | Updated the doc for new pg/coq. Made modifications advised by Stefan | Pierre Courtieu | 2005-02-17 |
| | | | | | Monnier on holes.el. | ||
| * | debugging the new holes-mode for fsf emacs. Keyboard shortcuts was | Pierre Courtieu | 2005-02-16 |
| | | | | | badly defined. | ||
| * | Update FAQ for X-Symbol large fonts (from Clemens Ballarin) | David Aspinall | 2005-02-15 |
| | | |||
| * | Modified holes doc string to fit to new shortcut of holes-mode. | Pierre Courtieu | 2005-02-15 |
| | | |||
| * | Changes from Clemens Ballarin for large X-Symbol fonts | David Aspinall | 2005-02-15 |
| | | |||
| * | New files. | David Aspinall | 2005-02-15 |
| | | |||
| * | Finished making holes.el a real minor-mode. There is a new file | Pierre Courtieu | 2005-02-15 |
| | | | | | | | | | | 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). | ||
| * | cleaning holes.el. All functions are prefixed with "holes-". Also | Pierre Courtieu | 2005-02-14 |
| | | | | | modified coq.el and coq-abbrev.el accordingly. | ||
| * | Starting to clean holes.el following Stefan Monnier's advices. Making | Pierre Courtieu | 2005-02-14 |
| | | | | | holes a real minor-mode. | ||
| * | Comments. | David Aspinall | 2005-02-13 |
| | | |||
| * | Force branch version | David Aspinall | 2005-02-13 |
| | | |||
| * | Added simple testing framework (in progress) | David Aspinall | 2005-02-13 |
| | | |||
 |
index : proof-general | |
| Emacs interface for proof assistants |
| aboutsummaryrefslogtreecommitdiffhomepage |