| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2005-09-30 | Add more user preferences, fix existing ones. | David Aspinall | |
| 2005-05-17 | Documentation. | David Aspinall | |
| 2005-04-21 | added some entris in coq menus. | Pierre Courtieu | |
| 2005-04-20 | cleaned a bit coq.el (checkdoc). Put some comments to tell what is to | Pierre Courtieu | |
| be removed when coq-8.0 becomes unsupported. | |||
| 2005-04-20 | New backtracking system for coq continues, this time it uses a new Coq | Pierre 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-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-02-17 | Updated the doc for new pg/coq. Made modifications advised by Stefan | Pierre Courtieu | |
| Monnier on holes.el. | |||
| 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-13 | Added simple testing framework (in progress) | David Aspinall | |
| 2005-02-10 | Deleted compatibility for coq v6 and v7 + new backtracking system. For | Pierre Courtieu | |
| now it can be triggered only by using coq-version-is-v8-1. | |||
| 2005-01-28 | Patch from Stefan Monnier: | David Aspinall | |
| 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. | |||
| 2004-09-14 | Add spaces after setting commands to separate. Temporarily disable ↵ | David Aspinall | |
| print-only-first-subgoal. | |||
| 2004-08-30 | debugged the indentation of coq (bug report of Batsiaan Zapf august | Pierre Courtieu | |
| 3rd 2004). I found another bug (infinite loop due to an error in coq-back-to-indentation-prevline). | |||
| 2004-08-25 | More proofgeneral.org removals | David Aspinall | |
| 2004-07-23 | Fixed Coq version detection at start. | Pierre Courtieu | |
| 2004-05-11 | adding the "Comments" keyword in state-preserving commands. | Pierre Courtieu | |
| 2004-05-09 | Set comment-quote-nested (for Emacs/XEmacs 21.5) | David Aspinall | |
| 2004-05-07 | added "User error" to error message (had already "User Error"). | Pierre Courtieu | |
| 2004-05-07 | Updated. | David Aspinall | |
| 2004-05-07 | New files. | David Aspinall | |
| 2004-05-06 | bug fix with terminal regexp (pb with :"unfold foo in |- *.") | Pierre Courtieu | |
| 2004-04-23 | fixed the need input_spec warning. | Pierre Courtieu | |
| 2004-04-23 | Adjust attempt at multiple file handling. Run make instead of coqc if find ↵ | David Aspinall | |
| a makefile. Begin handling requires. | |||
| 2004-04-23 | Updated. | David Aspinall | |
| 2004-04-23 | modified the syntax for subscript in coq/pg | Pierre Courtieu | |
| 2004-04-23 | deleted coq x symbols doc in CHANGES. | Pierre Courtieu | |
| 2004-04-22 | Tidy menus, add new commands | David Aspinall | |
| 2004-04-22 | Add extra user options, extra commands, start of new attempt at multiple file. | David Aspinall | |
| 2004-04-22 | Update to Coq 8.0 syntax | David Aspinall | |
| 2004-04-21 | Updated. | David Aspinall | |
| 2004-04-21 | Fix home page address, mention new menu option. | David Aspinall | |
| 2004-04-21 | Update for V8 syntax. | David Aspinall | |
| 2004-04-21 | Updated. | David Aspinall | |
| 2004-04-21 | Deleted the "3 buffers view menu entry" for coq, this is now a | Pierre Courtieu | |
| proofgeneral menu entry (bug of the 3.5 release). | |||
| 2004-04-17 | Updated. | David Aspinall | |
| 2004-04-17 | Compiler warnings | David Aspinall | |
| 2004-04-16 | little fix for x-symbols coq. | Pierre Courtieu | |
| 2004-04-16 | modified the noteq token (become '<>' ). | Pierre Courtieu | |
| 2004-04-16 | added an example fils for coq x-symbols. | Pierre Courtieu | |
| 2004-04-16 | New files. | David Aspinall | |
| 2004-04-15 | Updated. | David Aspinall | |
| 2004-04-15 | Fix typo. | David Aspinall | |
| 2004-04-15 | commented the new tarski example for coq. | Pierre Courtieu | |
| 2004-04-15 | added Knaster - Tarski theorem. | Pierre Courtieu | |
| 2004-04-15 | added some tactical names for coq. | Pierre Courtieu | |
| 2004-04-15 | Add doc for x-symbols | David Aspinall | |
| 2004-04-15 | little change in CHANGES and in coq syntax table. | Pierre Courtieu | |
| 2004-04-14 | Cleanup file by removing some unnecessary settings (I hope) | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |