aboutsummaryrefslogtreecommitdiff
path: root/coq
AgeCommit message (Collapse)Author
2004-04-21Deleted the "3 buffers view menu entry" for coq, this is now aPierre Courtieu
proofgeneral menu entry (bug of the 3.5 release).
2004-04-17Updated.David Aspinall
2004-04-17Compiler warningsDavid Aspinall
2004-04-16little fix for x-symbols coq.Pierre Courtieu
2004-04-16modified the noteq token (become '<>' ).Pierre Courtieu
2004-04-16added an example fils for coq x-symbols.Pierre Courtieu
2004-04-16New files.David Aspinall
2004-04-15Updated.David Aspinall
2004-04-15Fix typo.David Aspinall
2004-04-15commented the new tarski example for coq.Pierre Courtieu
2004-04-15added Knaster - Tarski theorem.Pierre Courtieu
2004-04-15added some tactical names for coq.Pierre Courtieu
2004-04-15Add doc for x-symbolsDavid Aspinall
2004-04-15little change in CHANGES and in coq syntax table.Pierre Courtieu
2004-04-14Cleanup file by removing some unnecessary settings (I hope)David Aspinall
2004-04-14Deleted fileDavid Aspinall
2004-04-14Updated.David Aspinall
2004-04-14added basic support for imenu for coq.Pierre Courtieu
2004-04-14added the "return" keyword to coqPierre Courtieu
2004-04-06added some commands in coq menuPierre Courtieu
2004-04-06fixed coq xsymb table.Pierre Courtieu
2004-04-05Fixed coq x-symbols. now alphaa is not encoded, aalpha is not encoded,Pierre Courtieu
but alpha_, _alpha and _alpha_ are decoded.
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
- __ makes the following word (if immediately after __) subscript - ^^ makes the following word (if immediately after ^^) superscript - __{...} makes ... subscript - ^^{...} makes ... superscript
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
x-symbol-isabelle.el. Seems to work.
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
indent-line-function).
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
<term>. which is a save command (but not a save giving a name like Save id.).
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
+ some menu modifications
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
does not use "proof-goal-command-p" and is not powerful enough.
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 23:58:01 +0000