aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2006-07-04fix the bug for coq indetation of two consecutive comments. Code isPierre Courtieu
ugly, should take the code given by Stefan Monnier and adapt it (it does not indent everything as is).
2006-07-04fix a bug in coq indentation (loop). seems to be fixed. I still have aPierre Courtieu
problem indenting comments (two consecutive comments: second shifted).
2006-07-04moving coq-goal-command-p to indetation code, as from v8.1, goals arePierre Courtieu
detected by the goal attribute of spans. syntactical goal recognizing is still used in indetation code, and for v8.0 compatibility. I shall remove v8.0 compatibility in some months.
2006-06-13section backtracking bug fixed.Pierre Courtieu
2006-05-26Stop texi2html complaining about unknown command @c=====David Aspinall
2006-05-26Set version tag for new release.David Aspinall
2006-05-26Fix to work with coq 8.1 again (havent tested 8.0)David Aspinall
2006-05-26Remove debugsDavid Aspinall
2006-05-26Add back 'raw-text setting, now LANG settings aren't taking effect again ↵David Aspinall
[me: XEmacs 21.4.19 on FC5]
2006-05-26Updated.David Aspinall
2006-05-26Updated.David Aspinall
2006-05-26Note about final 3.6 todoDavid Aspinall
2006-05-26Detect EMACS setting.David Aspinall
2006-05-26Add C-g watcher for trace bufferDavid Aspinall
2006-05-23Fix to remove mention of coding-system-for-write, coding-system-for-read not ↵David Aspinall
available on non-Mule compiles
2006-05-11Note about proof-shell-unicode setting.David Aspinall
2006-05-11Note about proof-shell-unicode setting.David Aspinall
2006-04-26Modified documentation abou file variables to be compliant with newPierre Courtieu
xxx-prog-args variabel.
2006-04-26Changed the type of proof-goal-command-p. It takes now a span, whichPierre Courtieu
allows using a span attribute to detect goal commands. I think I modified all modes accordingly.
2006-02-24back to using sym-lock ... x-symbol will not be supported anymore for PhoX + ↵Christophe Raffalli
imporvment in proof by contextual menu
2006-02-16made coq error regexp more precisePierre Courtieu
2006-02-14Set version tag for new release.David Aspinall
2006-02-14NoteDavid Aspinall
2006-02-14CommentsDavid Aspinall
2006-02-14Add example settings for coq-prog-args and coq-prog-envDavid Aspinall
2006-02-14Revert use of 'raw-text for coding-system-for-read/write since it changes ↵David Aspinall
behaviour in at least one Emacs version, causing PG to hang.
2006-02-14Add back lost editsDavid Aspinall
2006-02-14Add <PA>-prog-args and <PA>-prog-envDavid Aspinall
2006-02-13support nested blocks of super/sub-script, but only the outermost levelMakarius Wenzel
is actually displayed as such -- by Clemens Ballarin;
2006-02-12isar-preprocessing: replace \n by \<^newline>;Makarius Wenzel
2006-02-10isar-goals-font-lock-keywords: "abbreviations";Makarius Wenzel
2006-02-09Cleanup version testing, prevent crash in case version string doesn't match.David Aspinall
2006-01-28typo in coq.el for regexp of sections.Pierre Courtieu
2006-01-27Fix from PaulDavid Aspinall
2006-01-10commit of a small patch from Stefan Monnier, to fix a small bug ofPierre Courtieu
drag-mouse-region with holes.
2006-01-09PG 3.6: remove Info item from toolbar; it's not very useful and under ↵David Aspinall
PA->Help anyway
2006-01-08Fix for coloured face specs on AquaemacsDavid Aspinall
2006-01-05added \<setminus>;Makarius Wenzel
2005-11-28added some keyword to coq tacics.Pierre Courtieu
2005-11-25Added Module/EndDavid Aspinall
2005-11-25Fix Pierre's emailDavid Aspinall
2005-11-14actually revert to revision 8.15;Makarius Wenzel
2005-11-09Added holes to "math...with" generation from a type name.Pierre Courtieu
2005-11-09backtracking my change on functionPierre Courtieu
proof-shell-invisible-cmd-get-result, we will fix this better with David soon (use of the noerror arg).
2005-11-08TypoDavid Aspinall
2005-11-07added match...with automatic building from atype name.Pierre Courtieu
Had to correct a bug in proof-shell.
2005-10-20bug fixChristophe Raffalli
2005-10-12added lock and unlock for unification variablesChristophe Raffalli
2005-10-04Set version tag for new release.David Aspinall
2005-10-04Make install-bin also install Isabelle and Lego scriptsDavid Aspinall