aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
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
|
* Print Coercions added to coq-syntaxGravatar Assia Mahboubi2007-12-07
|
* Corollary added to Coq startersGravatar Assia Mahboubi2007-12-05
|
* coq solve tacs modifiedGravatar Assia Mahboubi2007-11-30
|
* colouring for Reserved NotationsGravatar Assia Mahboubi2007-11-26
|
* removed 'by'form coq-reserved and added it to coq-solve-tacticsGravatar Assia Mahboubi2007-11-20
|
* adding coq-solve tacticsGravatar Assia Mahboubi2007-11-20
|
* coq-user-reserved-db addedGravatar Assia Mahboubi2007-11-16
|
* test commit : added Structure to coq-defn-dbGravatar Assia Mahboubi2007-11-16
|
* Fix http://proofgeneral.inf.ed.ac.uk/trac/ticket/160Gravatar David Aspinall2007-11-12
|
* fixing small font-lock bug with ssreflect syntax.Gravatar Pierre Courtieu2007-11-08
|
* Debugging font-lock regexp.Gravatar Pierre Courtieu2007-11-07
|
* Menu are now correctly sorted.Gravatar Pierre Courtieu2007-11-07
|
* Debugging font-lock regexp.Gravatar Pierre Courtieu2007-11-07
|
* Debugging font-lock regexps. Bad order: longer regexp should be putGravatar Pierre Courtieu2007-11-07
| | | | first.
* Fixed colorization bugs reported by Assai MAhboubi, this commit isGravatar Pierre Courtieu2007-10-30
| | | | part of the previoous one (missused cvs).
* Fixed small colorizing bugs (when keywords contain sub words colorizedGravatar Pierre Courtieu2007-10-30
| | | | in another color). Reported by Assia Mahboubi.
* Bug fixed. Reported by Assia Mahboubi.Gravatar Pierre Courtieu2007-10-30
|
* Fixed a bug on custom vars (bad :type) + Added a customizable user varGravatar Pierre Courtieu2007-10-29
| | | | for tacticals (asked by Assi Mahboubi).
* Add support for sending back literal commands reusing PBP markup mechanisms.Gravatar David Aspinall2007-08-14
|
* Added new keywords.Gravatar Pierre Courtieu2007-07-12
|
* Fix #114: syntax highlighting mistake for identifiers beginning with fun/forall.Gravatar David Aspinall2007-05-25
|
* 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.
* Fixed the "Time Qed." mistreating (now recognized as a save commandGravatar Pierre Courtieu2007-04-26
| | | | and make spans agregation ok).
* Added some unknown keyword (not changing state). Fixes bug 113 from emakarov.MGravatar Pierre Courtieu2007-04-26
|
* Small fixes.Gravatar Pierre Courtieu2007-04-25
|
* small coloring fix.Gravatar Pierre Courtieu2007-04-23
|
* 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
|
* Added things in CHANGES.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.
* Made coq version 8.1 the default.Gravatar Pierre Courtieu2007-04-16
|
* Change in a regexp for coq-shell-prompt.Gravatar Pierre Courtieu2007-03-26
|
* *** empty log message ***Gravatar Pierre Courtieu2007-03-08
|
* Remove proof-indent-pad-eol atrocityGravatar David Aspinall2007-02-28
|
* Added some keywords ("Declare Module Import"...).Gravatar Pierre Courtieu2006-12-22
|
* 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
|