aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq.el
Commit message (Collapse)AuthorAge
* Emacs compatibility/API updates: string-to-int -> string-to-numberGravatar David Aspinall2007-12-10
|
* Fixup some compile warningsGravatar David Aspinall2007-12-09
|
* Add support for sending back literal commands reusing PBP markup mechanisms.Gravatar David Aspinall2007-08-14
|
* Fixed prompt regexp.Gravatar Pierre Courtieu2007-05-10
|
* Never use special chars with >= coq-8.1.Gravatar Pierre Courtieu2007-05-10
| | | | | proof-shell-unicode set to nil by default because of xemacs which needs a library for utf-8.
* Fixed coq prog persistent setting.Gravatar Pierre Courtieu2007-05-10
|
* Fixing auto shrink in coq three window mode, to avoid windowGravatar Pierre Courtieu2007-04-26
| | | | disappearing.
* Small fixes.Gravatar Pierre Courtieu2007-04-25
|
* Fixed bug 111. Scroll response window to see goal and as muchGravatar Pierre Courtieu2007-04-23
| | | | hypothesis as possible.
* Fixing bug 110 for SearchRewrite en SearchAbout coq commends.Gravatar Pierre Courtieu2007-04-23
|
* Adapting last features to fsf emacs.Gravatar Pierre Courtieu2007-04-23
|
* Adapting error highlighting (coq) to x-symbol.Gravatar Pierre Courtieu2007-04-20
|
* Add a shrink adapting hook for coq response buffer.Gravatar Pierre Courtieu2007-04-20
|
* Adding comments to experimental response buffer height adapting.Gravatar Pierre Courtieu2007-04-18
|
* Experimental feature: in three buffer mode: shrink response window asGravatar Pierre Courtieu2007-04-16
| | | | much as possible.
* Small fixes from Stefan Monnier.Gravatar Pierre Courtieu2007-04-16
|
* Patch from Stefan Monnier.Gravatar Pierre Courtieu2007-04-16
|
* Adapted to hybrid response/goals outputs from coq. We need somethingGravatar Pierre Courtieu2007-04-16
| | | | generic on that. Currently I use proof-shell-process-output-system-specific.
* Change in a regexp for coq-shell-prompt.Gravatar Pierre Courtieu2007-03-26
|
* Added completion to coq-prog-name asking.Gravatar Pierre Courtieu2006-12-13
|
* Fixed keyboard shortcuts.Gravatar Pierre Courtieu2006-12-12
|
* Fixed coq 8.0 compatibility and coq version detection.Gravatar Pierre Courtieu2006-12-12
|
* Error highlighting in coq only when scripting (not when sendingGravatar Pierre Courtieu2006-10-23
| | | | command invisibly).
* Fix for coq-utf-safe.Gravatar Pierre Courtieu2006-10-06
|
* utf safe coq mode is not linked to proof-shell-unicode, as unicode isGravatar Pierre Courtieu2006-09-29
| | | | not well handle by xemacs.
* adapting to proof-shell-unicode. Coq has not been adapted to theGravatar Pierre Courtieu2006-09-29
| | | | -emacs-U option.
* Simplified prompt regexp for coq, preparing new prompt delimitersGravatar Pierre Courtieu2006-09-29
| | | | <prompt> and </prompt>.
* fixed a bug with wakeup char for coq.Gravatar Pierre Courtieu2006-09-29
|
* Added \x6 as a possible wakeup char for coq. For the moment thisGravatar Pierre Courtieu2006-09-25
| | | | | special char is used when the -emacs-U is used (with or instead of -emacs) in cvs version of coq of today 25/9/2006.
* fix a bug with error highlighting. Not sure it is ok but seems toGravatar Pierre Courtieu2006-09-14
| | | | work.
* fixed a bug from Stefan Monnier.Gravatar Pierre Courtieu2006-09-14
|
* Fixed nested comment support for scripting, in xemacs (worked alreadyGravatar Pierre Courtieu2006-09-08
| | | | on GNU Emacs). Instanciated proof-parse-function for that...
* Making error highlighting more robust (for both emacsen) and use aGravatar Pierre Courtieu2006-09-06
| | | | span instead of region.
* Error highliting in coq now worksGravatar Pierre Courtieu2006-09-05
|
* still experimenting error highlitingGravatar Pierre Courtieu2006-09-05
|
* Experimenting highlighting the error from coqtop errorGravatar Pierre Courtieu2006-09-05
| | | | | message. Function work but proof-shell-handle-error-or-interrupt-hook does not allow to activate the region...
* Trying to mae indentation aware of nested comments (to be simplifiedGravatar Pierre Courtieu2006-09-04
| | | | | when xemacs will deal with nested comments). Seems to work, a bit slow.
* Small fixes on syntax tables.Gravatar Pierre Courtieu2006-08-25
|
* Adding commentsGravatar Pierre Courtieu2006-08-25
|
* Small fixes.Gravatar Pierre Courtieu2006-08-25
|
* Fixed a small bug in indentation of coq.Gravatar Pierre Courtieu2006-08-25
| | | | Fixed behavior for making abbrev table (don't if it already exists).
* Changed state-preserving check for coq.Gravatar Pierre Courtieu2006-08-24
|
* changed coq bqcktracking to avoid doing backtrack x y z when x y and zGravatar Pierre Courtieu2006-08-24
| | | | | | 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.
* fsf emacs compatibilty for symbol-at-point.Gravatar Pierre Courtieu2006-08-23
|
* Cleaning in coq and lib, fixed licenses and docstrings.Gravatar Pierre Courtieu2006-08-23
| | | | Added one or two details to docstring of generic variables.
* Making non recursive functions to make fsf emacs happy, not yet finished.Gravatar Pierre Courtieu2006-08-22
|
* Big redesign of the coq syntax defintion, centralization in big tablesGravatar Pierre Courtieu2006-08-22
| | | | like coq-commands-db.
* Menus redesign, new interactive tactics/commands/termsGravatar Pierre Courtieu2006-08-21
| | | | insertion. Great!
* Started the coq-insert-tactic.Gravatar Pierre Courtieu2006-08-21
|
* Moved the coq local variables tools in a separate file and made itGravatar Pierre Courtieu2006-08-17
| | | | simpler.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 14:01:22 +0000