Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Remove some old X-Symbol references. | 2009-09-01 | |
| | |||
* | Merge changes from Version4Branch. | 2008-07-24 | |
| | |||
* | Fixed indentation and goal display. | 2008-01-28 | |
| | |||
* | Patch and cleanup for Coq indent code, see ↵ | 2008-01-25 | |
| | | | | http://proofgeneral.inf.ed.ac.uk/trac/ticket/173 | ||
* | Missing paren | 2008-01-24 | |
| | |||
* | Fixes and cleanups for coq-indent-line, see Trac #172 | 2008-01-24 | |
| | |||
* | Remove proof-indent-pad-eol atrocity | 2007-02-28 | |
| | |||
* | typo in coq-indent. | 2006-09-15 | |
| | |||
* | fixed a typo in last correction. | 2006-09-15 | |
| | |||
* | fixed a bug from Stefan Monnier. | 2006-09-14 | |
| | |||
* | cleaning from Stefan Monnier. | 2006-09-13 | |
| | |||
* | cleaning from Stefan Monnier. | 2006-09-13 | |
| | |||
* | Fixed nested comment support for scripting, in xemacs (worked already | 2006-09-08 | |
| | | | | on GNU Emacs). Instanciated proof-parse-function for that... | ||
* | Trying to mae indentation aware of nested comments (to be simplified | 2006-09-04 | |
| | | | | | when xemacs will deal with nested comments). Seems to work, a bit slow. | ||
* | Fixed a small bug in indentation of coq. | 2006-08-25 | |
| | | | | Fixed behavior for making abbrev table (don't if it already exists). | ||
* | fixing a bug introduced lately (coq-save-command-p *needs* two args | 2006-08-24 | |
| | | | | beacause proof-save-command-p needs is so defined). | ||
* | Fixed indentation and font-lock for coq. Better, faster. | 2006-08-23 | |
| | |||
* | Coq indentation small fixes. | 2006-08-23 | |
| | |||
* | fsf emacs compatibilty for symbol-at-point. | 2006-08-23 | |
| | |||
* | removed debug messages from indentation code. | 2006-07-04 | |
| | |||
* | fix the bug for coq indetation of two consecutive comments. Code is | 2006-07-04 | |
| | | | | | ugly, should take the code given by Stefan Monnier and adapt it (it does not indent everything as is). | ||
* | fix a bug in coq indentation (loop). seems to be fixed. I still have a | 2006-07-04 | |
| | | | | problem indenting comments (two consecutive comments: second shifted). | ||
* | moving coq-goal-command-p to indetation code, as from v8.1, goals are | 2006-07-04 | |
| | | | | | | 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. | ||
* | added match...with automatic building from atype name. | 2005-11-07 | |
| | | | | Had to correct a bug in proof-shell. | ||
* | Finished making holes.el a real minor-mode. There is a new file | 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). | ||
* | debugged the indentation of coq (bug report of Batsiaan Zapf august | 2004-08-30 | |
| | | | | | 3rd 2004). I found another bug (infinite loop due to an error in coq-back-to-indentation-prevline). | ||
* | added the forall x-symbol to the indent keywords lists. | 2004-03-30 | |
| | |||
* | bug fix in holes (call to proof-indent-line instead of funcall | 2004-03-15 | |
| | | | | indent-line-function). | ||
* | little bug fix in coq-indent.el | 2004-03-15 | |
| | |||
* | bug fixes on indenting and command-end-regexp. | 2004-03-11 | |
| | |||
* | compile warning corrections | 2004-03-10 | |
| | |||
* | indentation for coq completely re-coded, because the generic mechanism | 2004-03-08 | |
does not use "proof-goal-command-p" and is not powerful enough. |