aboutsummaryrefslogtreecommitdiffhomepage
path: root/coq
Commit message (Collapse)AuthorAge
* 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
|
* 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
|
* unified example with other proof assistants;Gravatar Makarius Wenzel1999-09-24
|
* 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.
* Cleaned up example files so all demonstrate same theorem "conj_comms".Gravatar David Aspinall1999-09-13
| | | | | Would be nice to add more theorems to compare scripts in different systems.
* Set proof-{qed,save}-commands.Gravatar David Aspinall1999-09-13
|
* Updated from Coq 6.3 distrib.Gravatar David Aspinall1999-08-23
|
* Updates suggested by Markus and Patrick for Coq 6.3.Gravatar David Aspinall1999-08-23
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 21:25:04 +0000