aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
Commit message (Expand)AuthorAge
* added some commands in coq menuGravatar Pierre Courtieu2004-04-06
* fixed coq xsymb table.Gravatar Pierre Courtieu2004-04-06
* Fixed coq x-symbols. now alphaa is not encoded, aalpha is not encoded,Gravatar Pierre Courtieu2004-04-05
* Use official indentation\!Gravatar David Aspinall2004-04-02
* Remove three-buffer stuff (made generic)Gravatar David Aspinall2004-04-02
* changed ths syntax for sub/superscript:Gravatar Pierre Courtieu2004-04-01
* added subscript in x-symbols-coq.el.Gravatar Pierre Courtieu2004-03-31
* debugging coq-x-symbols.elGravatar Pierre Courtieu2004-03-30
* added the forall x-symbol to the indent keywords lists.Gravatar Pierre Courtieu2004-03-30
* Trying to put x-symbols for coq. By copyingGravatar Pierre Courtieu2004-03-30
* *** empty log message ***Gravatar Pierre Courtieu2004-03-29
* V8/V7 reserved keywords for coqGravatar Pierre Courtieu2004-03-29
* coq < 8.0 menu and abbrevs.Gravatar Pierre Courtieu2004-03-19
* adjusting to new syntax.Gravatar Pierre Courtieu2004-03-18
* 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 the abbreviation of Hint Rewrite.Gravatar Pierre Courtieu2004-03-16
* Added one entry in the coq insert command menu (hint rewrite).Gravatar Pierre Courtieu2004-03-16
* bug fix in holes (call to proof-indent-line instead of funcallGravatar Pierre Courtieu2004-03-15
* little bug fix in coq-indent.elGravatar Pierre Courtieu2004-03-15
* 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
* compile warning correctionsGravatar Pierre Courtieu2004-03-10
* indentation for coq completely re-coded, because the generic mechanismGravatar Pierre Courtieu2004-03-08
* Cleanup top-level forms (unused x binding)Gravatar David Aspinall2004-03-01
* setq-default -> defconst for module-kinds-tableGravatar David Aspinall2004-03-01
* Fix V7.4 -> V74Gravatar 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 lines in holes short doc. And some abbrevs for coq.Gravatar 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
* Avoid type error if coq program can't be found during startup.Gravatar David Aspinall2004-02-17
* Added some interface stuff:Gravatar Pierre Courtieu2004-02-11
* little error in the syntax corrected.Gravatar Pierre Courtieu2004-02-11
* adapting to coq-8.0.Gravatar Pierre Courtieu2004-02-06
* Rever to simplest exampleGravatar David Aspinall2003-10-05
* 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