aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq.el
Commit message (Expand)AuthorAge
* making holes.el cleaner, with the help of Stefan Monnier. I had toGravatar Pierre Courtieu2005-03-08
* Updated the doc for new pg/coq. Made modifications advised by StefanGravatar Pierre Courtieu2005-02-17
* Finished making holes.el a real minor-mode. There is a new fileGravatar Pierre Courtieu2005-02-15
* cleaning holes.el. All functions are prefixed with "holes-". AlsoGravatar Pierre Courtieu2005-02-14
* Deleted compatibility for coq v6 and v7 + new backtracking system. ForGravatar Pierre Courtieu2005-02-10
* Add spaces after setting commands to separate. Temporarily disable print-onl...Gravatar David Aspinall2004-09-14
* Set comment-quote-nested (for Emacs/XEmacs 21.5)Gravatar David Aspinall2004-05-09
* bug fix with terminal regexp (pb with :"unfold foo in |- *.")Gravatar Pierre Courtieu2004-05-06
* Adjust attempt at multiple file handling. Run make instead of coqc if find a...Gravatar David Aspinall2004-04-23
* Add extra user options, extra commands, start of new attempt at multiple file.Gravatar David Aspinall2004-04-22
* Compiler warningsGravatar David Aspinall2004-04-17
* added basic support for imenu for coq.Gravatar Pierre Courtieu2004-04-14
* Remove three-buffer stuff (made generic)Gravatar David Aspinall2004-04-02
* coq < 8.0 menu and abbrevs.Gravatar Pierre Courtieu2004-03-19
* coq menu twickingGravatar Pierre Courtieu2004-03-17
* menu, holes and abbrev made better.Gravatar Pierre Courtieu2004-03-17
* Added 'Notation' stuff to coq menu command insert.Gravatar Pierre Courtieu2004-03-16
* Added one entry in the coq insert command menu (hint rewrite).Gravatar Pierre Courtieu2004-03-16
* added proof-really-save-command-p to coq config, to deal with ProofGravatar Pierre Courtieu2004-03-11
* bug fixes on indenting and command-end-regexp.Gravatar Pierre Courtieu2004-03-11
* fixed coq command-end expression-regexp to deal with the token '..'Gravatar Pierre Courtieu2004-03-10
* modification to avoid compile warnings (end)Gravatar Pierre Courtieu2004-03-10
* added a menu for hole operationsGravatar Pierre Courtieu2004-03-10
* indentation for coq completely re-coded, because the generic mechanismGravatar Pierre Courtieu2004-03-08
* setq-default -> defconst for module-kinds-tableGravatar David Aspinall2004-03-01
* little changes of menu/holes/abbrev in coq/pgGravatar Pierre Courtieu2004-02-26
* added menu entries to tactic menusGravatar Pierre Courtieu2004-02-19
* added submenus for command insertion for coq. menu uses abbrevGravatar Pierre Courtieu2004-02-19
* added some menu entries for coq.Gravatar Pierre Courtieu2004-02-19
* Coq Abbrevs now make holes. I will add a menu with basic command.Gravatar Pierre Courtieu2004-02-18
* Added some interface stuff:Gravatar Pierre Courtieu2004-02-11
* adapting to coq-8.0.Gravatar Pierre Courtieu2004-02-06
* Make find-and-forget robust for proverproc regionsGravatar David Aspinall2003-06-05
* Fix some compile errorsGravatar David Aspinall2003-02-24
* corrected a bug of pg/coq, the following line was not recognized as aGravatar Pierre Courtieu2003-02-20
* Added documentation string to the variables coq-version-is-V6 (new),Gravatar Pierre Courtieu2003-02-16
* Fixes so that compile worksGravatar David Aspinall2003-02-15
* Added the keyword "Local :=" to the coq-goal-command-p function, likeGravatar Pierre Courtieu2003-02-12
* little modif on the end-cammand regexp.Gravatar Pierre Courtieu2003-02-10
* little change to proof-script-command-end-regexp, again, to deal withGravatar Pierre Courtieu2003-02-06
* Slight modification to proof-script-command-end-regexp in coq.el, toGravatar Pierre Courtieu2003-02-06
* New setting for parse cmdend regexp.Gravatar David Aspinall2003-02-05
* code cleaning + deals better with the new module system of Coq. DidGravatar Pierre Courtieu2003-02-03
* Bug correction in the find-and-forget function for coq: in Coq v74, noGravatar Pierre Courtieu2003-01-30
* Added a file for testing modules of coq (new version 7.4). Plus someGravatar Pierre Courtieu2003-01-29
* removed some garbage printing in coq/Gravatar Pierre Courtieu2003-01-24
* Modifications for support of Coq-7.3.1+ and above (new module system).Gravatar Pierre Courtieu2003-01-24
* Check on context menu doesn't seem useful.Gravatar David Aspinall2002-09-11
* Improved implementation of zap-commas font lock behaviour, patch from Stefan ...Gravatar David Aspinall2002-08-31
* mPatch from Stefan Monnier [buffer-substring].Gravatar David Aspinall2002-08-29