aboutsummaryrefslogtreecommitdiff
path: root/coq
AgeCommit message (Expand)Author
2002-06-08Default to /usr/bin/perlDavid Aspinall
2002-05-29Made a negative test to compute the number of "Back n" inPierre Courtieu
2002-05-29Modification of the coq-find-and-forget function, in order to use thePierre Courtieu
2002-05-29Added some new tactic namesPierre Courtieu
2002-01-16WhitespaceDavid Aspinall
2001-09-24Add Lemma to exclusion for coq-goal-command-p.David Aspinall
2001-09-09Coq/lego confusionDavid Aspinall
2001-09-09Bug in new parsing for coq, mentionDavid Aspinall
2001-09-03Add specific install instrs, rearrange.David Aspinall
2001-08-31Add auto-compile-vos experimental setting for automatic multiple files.David Aspinall
2001-08-28Added something in the doc about coq-version-is-V7, and made the setting ofPierre Courtieu
2001-08-28Change of proof span type back to goalsaveDavid Aspinall
2001-04-10Modification of proof-script-command-end-regexp to allow commandsPierre Courtieu
2001-03-20Added the config var proof-script-command-end-regexp fot coq V7.Pierre Courtieu
2001-02-26minor change in coq.el to allow to force version of coq, with variablePierre Courtieu
2000-12-20Experimental support for multiple file handling.David Aspinall
2000-11-27fixed spelling;Makarius Wenzel
2000-11-24Continuing Coq V7 compatibility work, Begin Silent -> Set Silent, etc...Pierre Courtieu
2000-11-24Add a little change to coq-find-and-forget to work betterPierre Courtieu
2000-11-23I am starting to make PG coqV7 compatible, I think the best is toPierre Courtieu
2000-10-02Note about alternative path to perlDavid Aspinall
2000-09-29added some comments in coq/todoPierre Courtieu
2000-09-29Make default path to perl be /usr/bin/perlDavid Aspinall
2000-09-29a little change in coq/x-symbol, nothingPierre Courtieu
2000-09-29A little work around for the bug of Coq concerning the restart thatPierre Courtieu
2000-09-29Added Uncaught exception errors in coq-error-regexp.Pierre Courtieu
2000-09-27Updated from docDavid Aspinall
2000-08-26nothing important, I forgot to undo something before my last commit inPierre Courtieu
2000-08-26Some changes for undoing with coq, handle user-defined tactics, inPierre Courtieu
2000-08-14enhancement of outline regexps for coq, now when hiding bodies, we seePierre Courtieu
2000-08-14enhancement of x-symbol for coq, philosophy is not encoded, and phi1 is,Pierre Courtieu
2000-07-16Removed some (hopefully redundant) requires.David Aspinall
2000-06-22somme little changes to make undo work betterPierre Courtieu
2000-06-08basic setup for new indentation code;Makarius Wenzel
2000-06-08proper indentation;Makarius Wenzel
2000-06-02Added 3 entries in the Coq menu: Print Check and HintsPierre Courtieu
2000-06-01Removed time setting, added proof-assistant-settings-cmd to init string, but ...David Aspinall
2000-06-01Added a couple of settings for CoqDavid Aspinall
2000-05-29Removed use of proof-terminal-string, added explicit terminators everywhere.David Aspinall
2000-05-29Changed keybindings for coq specific functionsDavid Aspinall
2000-05-26proof-defass-default -> defpgdefaultDavid Aspinall
2000-05-25Spurious newline causing patch to fall over.David Aspinall
2000-05-25Revert to previous path for perl, better default for non-linux. Linux uses R...David Aspinall
2000-05-25Change default path to perlDavid Aspinall
2000-05-16debugging coq menu for old Xemacs compatibility, David said he will do thisPierre Courtieu
2000-05-11Changes and compatibility fixes for specific menu/keybindings.David Aspinall
2000-05-02Added proof-assistant-keymap and commands for defining insert keys.David Aspinall
2000-05-01Added specific menu for Coq.David Aspinall
2000-04-07pbp-mode -> goals-modeDavid Aspinall
2000-04-07More decorationDavid Aspinall