| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2006-08-25 | Fixed a small bug in indentation of coq. | Pierre Courtieu | |
| Fixed behavior for making abbrev table (don't if it already exists). | |||
| 2006-08-24 | Changed state-preserving check for coq. | Pierre Courtieu | |
| 2006-08-24 | changed coq bqcktracking to avoid doing backtrack x y z when x y and z | Pierre Courtieu | |
| are identical to current ones. This is because Backtrack x y z is sometimes slow even in such cases. Hopefully this won't break synchronization. | |||
| 2006-08-24 | fixing a bug introduced lately (coq-save-command-p *needs* two args | Pierre Courtieu | |
| beacause proof-save-command-p needs is so defined). | |||
| 2006-08-23 | Fixed indentation and font-lock for coq. Better, faster. | Pierre Courtieu | |
| 2006-08-23 | Coq indentation small fixes. | Pierre Courtieu | |
| 2006-08-23 | fsf emacs compatibilty for symbol-at-point. | Pierre Courtieu | |
| 2006-08-23 | Cleaning in coq and lib, fixed licenses and docstrings. | Pierre Courtieu | |
| Added one or two details to docstring of generic variables. | |||
| 2006-08-23 | Finished making functions over big tables non recursive. Works with | Pierre Courtieu | |
| emacs. | |||
| 2006-08-22 | Making non recursive functions to make fsf emacs happy, not yet finished. | Pierre Courtieu | |
| 2006-08-22 | Big redesign of the coq syntax defintion, centralization in big tables | Pierre Courtieu | |
| like coq-commands-db. | |||
| 2006-08-21 | Menus redesign, new interactive tactics/commands/terms | Pierre Courtieu | |
| insertion. Great! | |||
| 2006-08-21 | Started the coq-insert-tactic. | Pierre Courtieu | |
| 2006-08-17 | Moved the coq local variables tools in a separate file and made it | Pierre Courtieu | |
| simpler. | |||
| 2006-08-17 | continue on the support for local variables list semi-automatic | Pierre Courtieu | |
| insertion. I put a new file in lib with basic tools for file variables lists. | |||
| 2006-08-16 | Added entries in coq menu, rearranged coq menu. | Pierre Courtieu | |
| Also added semi-automated setting of local file variables (*** Local Variables ***) coq-prog-name and coq-prog-args. | |||
| 2006-07-20 | fixed a bug with scripting with coq v8.0. | Pierre Courtieu | |
| 2006-07-04 | removed debug messages from indentation code. | Pierre Courtieu | |
| 2006-07-04 | fix the bug for coq indetation of two consecutive comments. Code is | Pierre Courtieu | |
| ugly, should take the code given by Stefan Monnier and adapt it (it does not indent everything as is). | |||
| 2006-07-04 | fix a bug in coq indentation (loop). seems to be fixed. I still have a | Pierre Courtieu | |
| problem indenting comments (two consecutive comments: second shifted). | |||
| 2006-07-04 | moving coq-goal-command-p to indetation code, as from v8.1, goals are | Pierre Courtieu | |
| detected by the goal attribute of spans. syntactical goal recognizing is still used in indetation code, and for v8.0 compatibility. I shall remove v8.0 compatibility in some months. | |||
| 2006-06-13 | section backtracking bug fixed. | Pierre Courtieu | |
| 2006-05-26 | Fix to work with coq 8.1 again (havent tested 8.0) | David Aspinall | |
| 2006-05-26 | Remove debugs | David Aspinall | |
| 2006-04-26 | Changed the type of proof-goal-command-p. It takes now a span, which | Pierre Courtieu | |
| allows using a span attribute to detect goal commands. I think I modified all modes accordingly. | |||
| 2006-02-16 | made coq error regexp more precise | Pierre Courtieu | |
| 2006-02-14 | Comments | David Aspinall | |
| 2006-02-14 | Add example settings for coq-prog-args and coq-prog-env | David Aspinall | |
| 2006-02-09 | Cleanup version testing, prevent crash in case version string doesn't match. | David Aspinall | |
| 2006-01-28 | typo in coq.el for regexp of sections. | Pierre Courtieu | |
| 2005-11-28 | added some keyword to coq tacics. | Pierre Courtieu | |
| 2005-11-25 | Added Module/End | David Aspinall | |
| 2005-11-25 | Fix Pierre's email | David Aspinall | |
| 2005-11-09 | Added holes to "math...with" generation from a type name. | Pierre Courtieu | |
| 2005-11-07 | added match...with automatic building from atype name. | Pierre Courtieu | |
| Had to correct a bug in proof-shell. | |||
| 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). | |||
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |