aboutsummaryrefslogtreecommitdiff
path: root/coq
AgeCommit message (Collapse)Author
2008-02-04Add mode documentationDavid Aspinall
2008-02-01coq:cutomizable bound variable highlight (finally working)Assia Mahboubi
2008-01-31Update versions here.David Aspinall
2008-01-31Updated.David Aspinall
2008-01-31Revert last change, shell-command-to-string gives error when calledDavid Aspinall
with c:\Program Files\blah due to space in filename. Code here needs reworking more heavily for out-of-the-box Windows working.
2008-01-31Use coq-prog-name when looking for library, not hard coded coqtopDavid Aspinall
2008-01-31Use proof-locate-executable so works out-of-the-box on Windows.David Aspinall
2008-01-31Remove CVS merge junk!David Aspinall
2008-01-31updated CHANGESAssia Mahboubi
added an example file in coq/
2008-01-30coq : sorry, reverting previous buggy customizationAssia Mahboubi
2008-01-30New files.David Aspinall
2008-01-30Added a boolean defcustom test to make optional the highlight of variablesAssia Mahboubi
2008-01-30coq : changing highlight of solve, adding ExportAssia Mahboubi
2008-01-28Added displaying of the number of goals in the modeline.Pierre Courtieu
2008-01-28Fixed indentation and goal display.Pierre Courtieu
2008-01-28Fixed a problem with a wrong side effect on syntax databases (whenPierre Courtieu
sorting for menus).
2008-01-25Patch and cleanup for Coq indent code, see ↵David Aspinall
http://proofgeneral.inf.ed.ac.uk/trac/ticket/173
2008-01-24Remove use of proof-assDavid Aspinall
2008-01-24Updated.David Aspinall
2008-01-24New files.David Aspinall
2008-01-24Missing parenDavid Aspinall
2008-01-24Fixes and cleanups for coq-indent-line, see Trac #172David Aspinall
2008-01-17Use featurep test for XEmacs. Set proof-shell-indentifier-under-mouse-cmd.David Aspinall
2008-01-16Updated.David Aspinall
2008-01-15Remove coq-utf-safeDavid Aspinall
2008-01-15Deleted fileDavid Aspinall
2008-01-15Many compatibility updates, bug fixes, rearrangements for compilation.David Aspinall
2008-01-03Fixed abbrev installation. + small fixes.Pierre Courtieu
2008-01-03Fixed the "proof completed" regexp.Pierre Courtieu
2007-12-14Require for defface macroDavid Aspinall
2007-12-14Fix compilation problems and rearrange startup settings for ↵David Aspinall
coq-prog-name,coq-prog-args
2007-12-14Remove eval-when, seems unreliableDavid Aspinall
2007-12-14Attempt to fix compile problemsDavid Aspinall
2007-12-14Improve loading; these tests are not functioning yetDavid Aspinall
2007-12-14coq-goal-command-str-p: Fix suspected typo shown up by compile warning.David Aspinall
2007-12-13Bind coqdoc-html to C-c % w to avoid clash with help key.David Aspinall
2007-12-13New files.David Aspinall
2007-12-13Renamed fileDavid Aspinall
2007-12-13Updated.David Aspinall
2007-12-13Deleted fileDavid Aspinall
2007-12-12Updated.David Aspinall
2007-12-12Added a sample file for utf8.Pierre Courtieu
2007-12-12Compatibility with coq trunk where some special symbols are removed.Pierre Courtieu
2007-12-10Emacs compatibility/API updates: string-to-int -> string-to-numberDavid Aspinall
2007-12-09Fixup some compile warningsDavid Aspinall
2007-12-07Print Coercions added to coq-syntaxAssia Mahboubi
2007-12-05Corollary added to Coq startersAssia Mahboubi
2007-11-30coq solve tacs modifiedAssia Mahboubi
2007-11-26colouring for Reserved NotationsAssia Mahboubi
2007-11-20removed 'by'form coq-reserved and added it to coq-solve-tacticsAssia Mahboubi
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-19 06:57:31 +0000