aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
Commit message (Collapse)AuthorAge
* nothing important, I forgot to undo something before my last commit inGravatar Pierre Courtieu2000-08-26
| | | | coq/x-symbol-coq.el
* Some changes for undoing with coq, handle user-defined tactics, inGravatar Pierre Courtieu2000-08-26
| | | | coq/coq-syntax.el and coq/coq.el.
* enhancement of outline regexps for coq, now when hiding bodies, we seeGravatar Pierre Courtieu2000-08-14
| | | | | completely definitions and theorems, but proof script are hidden (but can be blindly sent to the prover). Seems to work correctly.
* enhancement of x-symbol for coq, philosophy is not encoded, and phi1 is,Gravatar Pierre Courtieu2000-08-14
| | | | one problem remains: a word ending with phi will be encoded.
* Removed some (hopefully redundant) requires.Gravatar David Aspinall2000-07-16
|
* somme little changes to make undo work betterGravatar Pierre Courtieu2000-06-22
|
* basic setup for new indentation code;Gravatar Makarius Wenzel2000-06-08
|
* proper indentation;Gravatar Makarius Wenzel2000-06-08
|
* Added 3 entries in the Coq menu: Print Check and HintsGravatar Pierre Courtieu2000-06-02
|
* Removed time setting, added proof-assistant-settings-cmd to init string, but ↵Gravatar David Aspinall2000-06-01
| | | | commented out
* Added a couple of settings for CoqGravatar David Aspinall2000-06-01
|
* Removed use of proof-terminal-string, added explicit terminators everywhere.Gravatar David Aspinall2000-05-29
|
* Changed keybindings for coq specific functionsGravatar David Aspinall2000-05-29
|
* proof-defass-default -> defpgdefaultGravatar David Aspinall2000-05-26
|
* Spurious newline causing patch to fall over.Gravatar David Aspinall2000-05-25
|
* Revert to previous path for perl, better default for non-linux. Linux uses ↵Gravatar David Aspinall2000-05-25
| | | | RPM, where its fixed.
* Change default path to perlGravatar David Aspinall2000-05-25
|
* debugging coq menu for old Xemacs compatibility, David said he will do thisGravatar Pierre Courtieu2000-05-16
| | | | for other provers (already done ?).
* Changes and compatibility fixes for specific menu/keybindings.Gravatar David Aspinall2000-05-11
|
* Added proof-assistant-keymap and commands for defining insert keys.Gravatar David Aspinall2000-05-02
|
* Added specific menu for Coq.Gravatar David Aspinall2000-05-01
|
* pbp-mode -> goals-modeGravatar David Aspinall2000-04-07
|
* More decorationGravatar David Aspinall2000-04-07
|
* Fixed up proof-shell-proof-completed mess nicely.Gravatar David Aspinall2000-04-07
|
* 3.1 not 3.2 changeGravatar David Aspinall2000-03-24
|
* Removed spurious requiresGravatar David Aspinall2000-03-24
|
* Updated to add me.Gravatar David Aspinall2000-03-23
|
* Updated todo's.Gravatar David Aspinall2000-03-22
|
* Switch back to %s, rename proof-shell-string-escapes -> ↵Gravatar David Aspinall2000-03-22
| | | | proof-shell-filename-escapes, and always apply for filename substn.
* Altered syntax a little bit so reset works for Section.Gravatar David Aspinall2000-03-19
|
* UpdatedGravatar David Aspinall2000-03-19
|
* Added settings for silent control. Also some minor support for Section.Gravatar David Aspinall2000-03-19
|
* Note about useless output from CoqGravatar David Aspinall2000-03-14
|
* Added proof-shell-{start,stop}-silent-cmd.Gravatar David Aspinall2000-03-14
|
* BUGS for Coq.Gravatar David Aspinall2000-03-13
|
* New/updated information filesGravatar David Aspinall2000-03-13
|
* Updated headers.Gravatar David Aspinall2000-03-09
|
* Added README files for each prover, summarizing status.Gravatar David Aspinall2000-03-09
|
* Split low-level todo into several files.Gravatar David Aspinall2000-03-08
|
* Fixes for short output duplication problem: set ↵Gravatar David Aspinall2000-01-06
| | | | proof-shell-eager-annotation-start-length.
* Use auto multiple files until something better comes alongGravatar David Aspinall1999-11-16
|
* Remove xi, appears in exists.Gravatar David Aspinall1999-11-15
|
* Added some greek letters. A mess if they occur in words.Gravatar David Aspinall1999-11-15
|
* Removed font-lock settings. Set proof-font-lock-zap-commas=tGravatar David Aspinall1999-11-15
|
* proof-nested-goals-allowed -> proof-completed-proof-behaviourGravatar David Aspinall1999-11-14
| | | | | Patch for more flexible handling of closing goal...save regions after proof has been completed.
* Experiment with X-Symbol support for Coq.Gravatar David Aspinall1999-11-13
|
* Call proof-goals-config-done properly.Gravatar David Aspinall1999-11-13
|
* Use infix syntaxGravatar David Aspinall1999-11-13
|
* Set font-lock-keywords before calling proof-config-done.Gravatar David Aspinall1999-11-12
|
* fixed indentation bug: use proof-looking-at (proof-case-fold-search);Gravatar Makarius Wenzel1999-11-10
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-20 20:15:43 +0000