aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq/coq.el
Commit message (Collapse)AuthorAge
* 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.
* 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
|
* 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
|
* 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
|
* 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
|
* Switch back to %s, rename proof-shell-string-escapes -> ↵Gravatar David Aspinall2000-03-22
| | | | proof-shell-filename-escapes, and always apply for filename substn.
* Added settings for silent control. Also some minor support for Section.Gravatar David Aspinall2000-03-19
|
* Added proof-shell-{start,stop}-silent-cmd.Gravatar David Aspinall2000-03-14
|
* 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
|
* 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.
* Call proof-goals-config-done properly.Gravatar 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
|
* Changed name of proof-shell-cd-cmd for uniformity.Gravatar David Aspinall1999-10-21
|
* This a try for commit, just changed the name of the maintainer of coq.elGravatar Pierre Courtieu1999-10-12
| | | | by my name Pierre Courtieu.
* Fix for Unnamed_thm: Coq really uses this identifier.Gravatar David Aspinall1999-10-06
|
* More improvements/fixes for closing unfinished proofs.Gravatar David Aspinall1999-10-06
| | | | Added proof-unnamed-theorem-name.
* Made new command proof-cd to cd to the directory of the currentGravatar David Aspinall1999-10-06
| | | | | | buffer. Added a version of it to proof-activate-scripting-hook. Removed cd from initialization sequence. Changed prover specifics accordingly.
* Fixed proof-showproof-commandGravatar David Aspinall1999-10-06
|
* Fixed coq-interrupt-regexp.Gravatar David Aspinall1999-10-06
|
* Remove coq-Search function, now generic.Gravatar David Aspinall1999-10-06
|
* Renamed some configuration variables for uniformity, see CHANGES.Gravatar David Aspinall1999-10-01
|
* Disable proof-help-string, was set to an invalid command.Gravatar David Aspinall1999-10-01
|
* Set proof-find-theorems-commandGravatar David Aspinall1999-09-23
|
* proof-completed-regexp: match number 1 is response text;Gravatar Makarius Wenzel1999-09-22
|
* Failed attempt to prevent Coq from starting up with display of current ↵Gravatar David Aspinall1999-09-13
| | | | directory.
* Set proof-{qed,save}-commands.Gravatar David Aspinall1999-09-13
|
* Missing parentheses added. Docstring fix.Gravatar David Aspinall1999-06-30
|
* last commit for 2.1Gravatar Patrick Loiseleur1999-06-30
|
* better syntaxGravatar Patrick Loiseleur1999-06-16
|
* Various updates. coq-end-Section now works properly.Gravatar Patrick Loiseleur1999-06-14
|
* various fixesGravatar Patrick Loiseleur1999-06-08
|
* renamed proof-commands-regexp to proof-indent-commands-regexp, whichGravatar Makarius Wenzel1999-05-27
| | | | is less confusing);
* closed string in comment;Gravatar Makarius Wenzel1999-05-26
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 23:34:17 +0000