index
:
proof-general
master
Emacs plugins for proof management systems
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
coq
/
coq.el
Age
Commit message (
Expand
)
Author
2008-01-28
Added displaying of the number of goals in the modeline.
Pierre Courtieu
2008-01-28
Fixed indentation and goal display.
Pierre Courtieu
2008-01-28
Fixed a problem with a wrong side effect on syntax databases (when
Pierre Courtieu
2008-01-24
Fixes and cleanups for coq-indent-line, see Trac #172
David Aspinall
2008-01-17
Use featurep test for XEmacs. Set proof-shell-indentifier-under-mouse-cmd.
David Aspinall
2008-01-15
Remove coq-utf-safe
David Aspinall
2008-01-15
Many compatibility updates, bug fixes, rearrangements for compilation.
David Aspinall
2008-01-03
Fixed abbrev installation. + small fixes.
Pierre Courtieu
2008-01-03
Fixed the "proof completed" regexp.
Pierre Courtieu
2007-12-14
Fix compilation problems and rearrange startup settings for coq-prog-name,coq...
David Aspinall
2007-12-14
Attempt to fix compile problems
David Aspinall
2007-12-12
Compatibility with coq trunk where some special symbols are removed.
Pierre Courtieu
2007-12-10
Emacs compatibility/API updates: string-to-int -> string-to-number
David Aspinall
2007-12-09
Fixup some compile warnings
David Aspinall
2007-08-14
Add support for sending back literal commands reusing PBP markup mechanisms.
David Aspinall
2007-05-10
Fixed prompt regexp.
Pierre Courtieu
2007-05-10
Never use special chars with >= coq-8.1.
Pierre Courtieu
2007-05-10
Fixed coq prog persistent setting.
Pierre Courtieu
2007-04-26
Fixing auto shrink in coq three window mode, to avoid window
Pierre Courtieu
2007-04-25
Small fixes.
Pierre Courtieu
2007-04-23
Fixed bug 111. Scroll response window to see goal and as much
Pierre Courtieu
2007-04-23
Fixing bug 110 for SearchRewrite en SearchAbout coq commends.
Pierre Courtieu
2007-04-23
Adapting last features to fsf emacs.
Pierre Courtieu
2007-04-20
Adapting error highlighting (coq) to x-symbol.
Pierre Courtieu
2007-04-20
Add a shrink adapting hook for coq response buffer.
Pierre Courtieu
2007-04-18
Adding comments to experimental response buffer height adapting.
Pierre Courtieu
2007-04-16
Experimental feature: in three buffer mode: shrink response window as
Pierre Courtieu
2007-04-16
Small fixes from Stefan Monnier.
Pierre Courtieu
2007-04-16
Patch from Stefan Monnier.
Pierre Courtieu
2007-04-16
Adapted to hybrid response/goals outputs from coq. We need something
Pierre Courtieu
2007-03-26
Change in a regexp for coq-shell-prompt.
Pierre Courtieu
2006-12-13
Added completion to coq-prog-name asking.
Pierre Courtieu
2006-12-12
Fixed keyboard shortcuts.
Pierre Courtieu
2006-12-12
Fixed coq 8.0 compatibility and coq version detection.
Pierre Courtieu
2006-10-23
Error highlighting in coq only when scripting (not when sending
Pierre Courtieu
2006-10-06
Fix for coq-utf-safe.
Pierre Courtieu
2006-09-29
utf safe coq mode is not linked to proof-shell-unicode, as unicode is
Pierre Courtieu
2006-09-29
adapting to proof-shell-unicode. Coq has not been adapted to the
Pierre Courtieu
2006-09-29
Simplified prompt regexp for coq, preparing new prompt delimiters
Pierre Courtieu
2006-09-29
fixed a bug with wakeup char for coq.
Pierre Courtieu
2006-09-25
Added \x6 as a possible wakeup char for coq. For the moment this
Pierre Courtieu
2006-09-14
fix a bug with error highlighting. Not sure it is ok but seems to
Pierre Courtieu
2006-09-14
fixed a bug from Stefan Monnier.
Pierre Courtieu
2006-09-08
Fixed nested comment support for scripting, in xemacs (worked already
Pierre Courtieu
2006-09-06
Making error highlighting more robust (for both emacsen) and use a
Pierre Courtieu
2006-09-05
Error highliting in coq now works
Pierre Courtieu
2006-09-05
still experimenting error highliting
Pierre Courtieu
2006-09-05
Experimenting highlighting the error from coqtop error
Pierre Courtieu
2006-09-04
Trying to mae indentation aware of nested comments (to be simplified
Pierre Courtieu
2006-08-25
Small fixes on syntax tables.
Pierre Courtieu
[next]