aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2005-05-31Key bindings for proof-shell-exit, proof-shell-start.David Aspinall
2005-05-31Comments.David Aspinall
2005-05-31Document proof-shell-start, proof-shell-exit keysDavid Aspinall
2005-05-31use physical path;Makarius Wenzel
2005-05-31tuned;Makarius Wenzel
2005-05-22removed find_rwrites, print_intros;Makarius Wenzel
2005-05-17Updated.David Aspinall
2005-05-17Fix menu path to CustomizeDavid Aspinall
2005-05-17Set version tag for new release.David Aspinall
2005-05-17- Don't just reuse visible frames but also iconified ones.David Aspinall
- 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.
2005-05-17Documentation.David Aspinall
2005-05-17Disable Twelf support by defaultDavid Aspinall
2005-05-17Fix the removal of ".UTF-8" from LANG.David Aspinall
2005-05-17Updated.David Aspinall
2005-05-17Add 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
- Basically rewrite span-overlay.el to better use the built-in overlay facilities. - Complain about the namespace pollution in span*.el.
2005-05-17Deleted fileDavid Aspinall
2005-05-17Updated.David Aspinall
2005-05-17added -L option;Makarius Wenzel
tuned;
2005-05-10undeleted;Makarius Wenzel
2005-04-27Add FAQ about favouritesDavid Aspinall
2005-04-21added some entris in coq menus.Pierre Courtieu
2005-04-20cleaned a bit coq.el (checkdoc). Put some comments to tell what is toPierre Courtieu
be removed when coq-8.0 becomes unsupported.
2005-04-20New backtracking system for coq continues, this time it uses a new CoqPierre Courtieu
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.
2005-03-25Updated.David Aspinall
2005-03-25New files.David Aspinall
2005-03-25Set version tag for new release.David Aspinall
2005-03-25Updated.David Aspinall
2005-03-25Remove project todosDavid Aspinall
2005-03-25Remove junkDavid Aspinall
2005-03-23Deleted fileDavid Aspinall
2005-03-23Use another symbolDavid Aspinall
2005-03-23Changes from Clemens Ballarin for large X-Symbol fontsDavid Aspinall
2005-03-23New files.David Aspinall
2005-03-23Large fontsDavid Aspinall
2005-03-21Updated.David Aspinall
2005-03-21Mention Stefan's patchesDavid Aspinall
2005-03-10debugging and cleaning of holes.el.Pierre Courtieu
2005-03-08small modifications, updating doc string of holes.el.Pierre Courtieu
2005-03-08making holes.el cleaner, with the help of Stefan Monnier. I had toPierre Courtieu
adapt coq.el to these modifications.
2005-03-01cleaning holes.el, starting to making it compatible with skeletons.Pierre Courtieu
2005-03-01debugging of holes.el.Pierre Courtieu
2005-02-21Debugging holes.el, starting trying to use skeletons.Pierre Courtieu
2005-02-21Cleaning file holes.el (tab-width, docstring etc).Pierre Courtieu
2005-02-17Updated the doc for new pg/coq. Made modifications advised by StefanPierre Courtieu
Monnier on holes.el.
2005-02-16debugging the new holes-mode for fsf emacs. Keyboard shortcuts wasPierre Courtieu
badly defined.
2005-02-15Update FAQ for X-Symbol large fonts (from Clemens Ballarin)David Aspinall
2005-02-15Modified holes doc string to fit to new shortcut of holes-mode.Pierre Courtieu
2005-02-15Changes from Clemens Ballarin for large X-Symbol fontsDavid Aspinall