aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
...
* added -L option;Gravatar Makarius Wenzel2005-05-17
| | | | tuned;
* undeleted;Gravatar Makarius Wenzel2005-05-10
|
* Add FAQ about favouritesGravatar David Aspinall2005-04-27
|
* added some entris in coq menus.Gravatar Pierre Courtieu2005-04-21
|
* cleaned a bit coq.el (checkdoc). Put some comments to tell what is toGravatar Pierre Courtieu2005-04-20
| | | | be removed when coq-8.0 becomes unsupported.
* New backtracking system for coq continues, this time it uses a new CoqGravatar Pierre Courtieu2005-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.Gravatar David Aspinall2005-03-25
|
* New files.Gravatar David Aspinall2005-03-25
|
* Set version tag for new release.Gravatar David Aspinall2005-03-25
|
* Updated.Gravatar David Aspinall2005-03-25
|
* Remove project todosGravatar David Aspinall2005-03-25
|
* Remove junkGravatar David Aspinall2005-03-25
|
* Deleted fileGravatar David Aspinall2005-03-23
|
* Use another symbolGravatar David Aspinall2005-03-23
|
* Changes from Clemens Ballarin for large X-Symbol fontsGravatar David Aspinall2005-03-23
|
* New files.Gravatar David Aspinall2005-03-23
|
* Large fontsGravatar David Aspinall2005-03-23
|
* Updated.Gravatar David Aspinall2005-03-21
|
* Mention Stefan's patchesGravatar David Aspinall2005-03-21
|
* debugging and cleaning of holes.el.Gravatar Pierre Courtieu2005-03-10
|
* small modifications, updating doc string of holes.el.Gravatar Pierre Courtieu2005-03-08
|
* making holes.el cleaner, with the help of Stefan Monnier. I had toGravatar Pierre Courtieu2005-03-08
| | | | adapt coq.el to these modifications.
* cleaning holes.el, starting to making it compatible with skeletons.Gravatar Pierre Courtieu2005-03-01
|
* debugging of holes.el.Gravatar Pierre Courtieu2005-03-01
|
* Debugging holes.el, starting trying to use skeletons.Gravatar Pierre Courtieu2005-02-21
|
* Cleaning file holes.el (tab-width, docstring etc).Gravatar Pierre Courtieu2005-02-21
|
* Updated the doc for new pg/coq. Made modifications advised by StefanGravatar Pierre Courtieu2005-02-17
| | | | Monnier on holes.el.
* debugging the new holes-mode for fsf emacs. Keyboard shortcuts wasGravatar Pierre Courtieu2005-02-16
| | | | badly defined.
* Update FAQ for X-Symbol large fonts (from Clemens Ballarin)Gravatar David Aspinall2005-02-15
|
* Modified holes doc string to fit to new shortcut of holes-mode.Gravatar Pierre Courtieu2005-02-15
|
* Changes from Clemens Ballarin for large X-Symbol fontsGravatar David Aspinall2005-02-15
|
* New files.Gravatar David Aspinall2005-02-15
|
* Finished making holes.el a real minor-mode. There is a new fileGravatar Pierre Courtieu2005-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-". AlsoGravatar Pierre Courtieu2005-02-14
| | | | modified coq.el and coq-abbrev.el accordingly.
* Starting to clean holes.el following Stefan Monnier's advices. MakingGravatar Pierre Courtieu2005-02-14
| | | | holes a real minor-mode.
* Comments.Gravatar David Aspinall2005-02-13
|
* Force branch versionGravatar David Aspinall2005-02-13
|
* Added simple testing framework (in progress)Gravatar David Aspinall2005-02-13
|
* Remove setting of x-symbol-language by C Raffalli.Gravatar David Aspinall2005-02-13
|
* Add patch by Stefan Monnier to revert frame titles (although would have ↵Gravatar David Aspinall2005-02-13
| | | | liked to keep them maybe)
* Add suggestion by Stefan Monnier (comment only)Gravatar David Aspinall2005-02-13
|
* Attempt to address X-Symbol startup problems for PhoX.Gravatar David Aspinall2005-02-13
|
* Deleted compatibility for coq v6 and v7 + new backtracking system. ForGravatar Pierre Courtieu2005-02-10
| | | | now it can be triggered only by using coq-version-is-v8-1.
* *** empty log message ***Gravatar Christophe Raffalli2005-02-09
|
* FAQ #1 typoGravatar David Aspinall2005-02-01
|
* Patch from Stefan Monnier:Gravatar David Aspinall2005-01-28
| | | | | | | | The * of (* is not quoted in the font-lock keywords leading to the possibility of matching the empty string, which tends to put font-lock in an infinite loop. Actually I think the infinite looping is due to a local bug in my experimental Emacs code, but the \\ is needed in order to really match what was intended.
* Mention to check FAQ tooGravatar David Aspinall2005-01-07
|
* changes to pbrpmGravatar Christophe Raffalli2004-12-08
|
* Name change of TODO/BUGS filesGravatar David Aspinall2004-12-01
|
* Renamed fileGravatar David Aspinall2004-12-01
|