aboutsummaryrefslogtreecommitdiff
path: root/coq/coq.el
AgeCommit message (Expand)Author
2006-08-17continue on the support for local variables list semi-automaticPierre Courtieu
2006-08-16Added entries in coq menu, rearranged coq menu.Pierre Courtieu
2006-07-20fixed a bug with scripting with coq v8.0.Pierre Courtieu
2006-05-26Remove debugsDavid Aspinall
2006-04-26Changed the type of proof-goal-command-p. It takes now a span, whichPierre Courtieu
2006-02-14CommentsDavid Aspinall
2006-02-14Add example settings for coq-prog-args and coq-prog-envDavid Aspinall
2006-01-28typo in coq.el for regexp of sections.Pierre Courtieu
2005-11-25Fix Pierre's emailDavid Aspinall
2005-11-09Added holes to "math...with" generation from a type name.Pierre Courtieu
2005-11-07added match...with automatic building from atype name.Pierre Courtieu
2005-09-30Add more user preferences, fix existing ones.David Aspinall
2005-04-21added some entris in coq menus.Pierre Courtieu
2005-04-20cleaned a bit coq.el (checkdoc). Put some comments to tell what is toPierre Courtieu
2005-04-20New backtracking system for coq continues, this time it uses a new CoqPierre Courtieu
2005-03-08making holes.el cleaner, with the help of Stefan Monnier. I had toPierre Courtieu
2005-02-17Updated the doc for new pg/coq. Made modifications advised by StefanPierre Courtieu
2005-02-15Finished making holes.el a real minor-mode. There is a new filePierre Courtieu
2005-02-14cleaning holes.el. All functions are prefixed with "holes-". AlsoPierre Courtieu
2005-02-10Deleted compatibility for coq v6 and v7 + new backtracking system. ForPierre Courtieu
2004-09-14Add spaces after setting commands to separate. Temporarily disable print-onl...David Aspinall
2004-05-09Set comment-quote-nested (for Emacs/XEmacs 21.5)David Aspinall
2004-05-06bug fix with terminal regexp (pb with :"unfold foo in |- *.")Pierre Courtieu
2004-04-23Adjust attempt at multiple file handling. Run make instead of coqc if find a...David Aspinall
2004-04-22Add extra user options, extra commands, start of new attempt at multiple file.David Aspinall
2004-04-17Compiler warningsDavid Aspinall
2004-04-14added basic support for imenu for coq.Pierre Courtieu
2004-04-02Remove three-buffer stuff (made generic)David Aspinall
2004-03-19coq < 8.0 menu and abbrevs.Pierre Courtieu
2004-03-17coq menu twickingPierre Courtieu
2004-03-17menu, holes and abbrev made better.Pierre Courtieu
2004-03-16Added 'Notation' stuff to coq menu command insert.Pierre Courtieu
2004-03-16Added one entry in the coq insert command menu (hint rewrite).Pierre Courtieu
2004-03-11added proof-really-save-command-p to coq config, to deal with ProofPierre Courtieu
2004-03-11bug fixes on indenting and command-end-regexp.Pierre Courtieu
2004-03-10fixed coq command-end expression-regexp to deal with the token '..'Pierre Courtieu
2004-03-10modification to avoid compile warnings (end)Pierre Courtieu
2004-03-10added a menu for hole operationsPierre Courtieu
2004-03-08indentation for coq completely re-coded, because the generic mechanismPierre Courtieu
2004-03-01setq-default -> defconst for module-kinds-tableDavid Aspinall
2004-02-26little changes of menu/holes/abbrev in coq/pgPierre Courtieu
2004-02-19added menu entries to tactic menusPierre Courtieu
2004-02-19added submenus for command insertion for coq. menu uses abbrevPierre Courtieu
2004-02-19added some menu entries for coq.Pierre Courtieu
2004-02-18Coq Abbrevs now make holes. I will add a menu with basic command.Pierre Courtieu
2004-02-11Added some interface stuff:Pierre Courtieu
2004-02-06adapting to coq-8.0.Pierre Courtieu
2003-06-05Make find-and-forget robust for proverproc regionsDavid Aspinall
2003-02-24Fix some compile errorsDavid Aspinall
2003-02-20corrected a bug of pg/coq, the following line was not recognized as aPierre Courtieu