aboutsummaryrefslogtreecommitdiff
path: root/coq
AgeCommit message (Expand)Author
2004-04-02Use official indentation\!David Aspinall
2004-04-02Remove three-buffer stuff (made generic)David Aspinall
2004-04-01changed ths syntax for sub/superscript:Pierre Courtieu
2004-03-31added subscript in x-symbols-coq.el.Pierre Courtieu
2004-03-30debugging coq-x-symbols.elPierre Courtieu
2004-03-30added the forall x-symbol to the indent keywords lists.Pierre Courtieu
2004-03-30Trying to put x-symbols for coq. By copyingPierre Courtieu
2004-03-29*** empty log message ***Pierre Courtieu
2004-03-29V8/V7 reserved keywords for coqPierre Courtieu
2004-03-19coq < 8.0 menu and abbrevs.Pierre Courtieu
2004-03-18adjusting to new syntax.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 the abbreviation of Hint Rewrite.Pierre Courtieu
2004-03-16Added one entry in the coq insert command menu (hint rewrite).Pierre Courtieu
2004-03-15bug fix in holes (call to proof-indent-line instead of funcallPierre Courtieu
2004-03-15little bug fix in coq-indent.elPierre 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-10compile warning correctionsPierre Courtieu
2004-03-08indentation for coq completely re-coded, because the generic mechanismPierre Courtieu
2004-03-01Cleanup top-level forms (unused x binding)David Aspinall
2004-03-01setq-default -> defconst for module-kinds-tableDavid Aspinall
2004-03-01Fix V7.4 -> V74David 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 lines in holes short doc. And some abbrevs for coq.Pierre 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-17Avoid type error if coq program can't be found during startup.David Aspinall
2004-02-11Added some interface stuff:Pierre Courtieu
2004-02-11little error in the syntax corrected.Pierre Courtieu
2004-02-06adapting to coq-8.0.Pierre Courtieu
2003-10-05Rever to simplest exampleDavid Aspinall
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
2003-02-16Added documentation string to the variables coq-version-is-V6 (new),Pierre Courtieu
2003-02-15Fixes so that compile worksDavid Aspinall
2003-02-12Added the keyword "Local :=" to the coq-goal-command-p function, likePierre Courtieu
2003-02-10little modif on the end-cammand regexp.Pierre Courtieu
2003-02-06little change to proof-script-command-end-regexp, again, to deal withPierre Courtieu
2003-02-06Slight modification to proof-script-command-end-regexp in coq.el, toPierre Courtieu
2003-02-05New setting for parse cmdend regexp.David Aspinall
2003-02-04Coq/pg: fixed a little bug with the "Print Hint" state preservingPierre Courtieu
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 12:33:16 +0000