aboutsummaryrefslogtreecommitdiff
path: root/coq
AgeCommit message (Collapse)Author
2000-04-07pbp-mode -> goals-modeDavid Aspinall
2000-04-07More decorationDavid Aspinall
2000-04-07Fixed up proof-shell-proof-completed mess nicely.David Aspinall
2000-03-243.1 not 3.2 changeDavid Aspinall
2000-03-24Removed spurious requiresDavid Aspinall
2000-03-23Updated to add me.David Aspinall
2000-03-22Updated todo's.David Aspinall
2000-03-22Switch back to %s, rename proof-shell-string-escapes -> ↵David Aspinall
proof-shell-filename-escapes, and always apply for filename substn.
2000-03-19Altered syntax a little bit so reset works for Section.David Aspinall
2000-03-19UpdatedDavid Aspinall
2000-03-19Added settings for silent control. Also some minor support for Section.David Aspinall
2000-03-14Note about useless output from CoqDavid Aspinall
2000-03-14Added proof-shell-{start,stop}-silent-cmd.David Aspinall
2000-03-13BUGS for Coq.David Aspinall
2000-03-13New/updated information filesDavid Aspinall
2000-03-09Updated headers.David Aspinall
2000-03-09Added README files for each prover, summarizing status.David Aspinall
2000-03-08Split low-level todo into several files.David Aspinall
2000-01-06Fixes for short output duplication problem: set ↵David Aspinall
proof-shell-eager-annotation-start-length.
1999-11-16Use auto multiple files until something better comes alongDavid Aspinall
1999-11-15Remove xi, appears in exists.David Aspinall
1999-11-15Added some greek letters. A mess if they occur in words.David Aspinall
1999-11-15Removed font-lock settings. Set proof-font-lock-zap-commas=tDavid Aspinall
1999-11-14proof-nested-goals-allowed -> proof-completed-proof-behaviourDavid Aspinall
Patch for more flexible handling of closing goal...save regions after proof has been completed.
1999-11-13Experiment with X-Symbol support for Coq.David Aspinall
1999-11-13Call proof-goals-config-done properly.David Aspinall
1999-11-13Use infix syntaxDavid Aspinall
1999-11-12Set font-lock-keywords before calling proof-config-done.David Aspinall
1999-11-10fixed indentation bug: use proof-looking-at (proof-case-fold-search);Makarius Wenzel
1999-10-21Changed name of proof-shell-cd-cmd for uniformity.David Aspinall
1999-10-12This a try for commit, just changed the name of the maintainer of coq.elPierre Courtieu
by my name Pierre Courtieu.
1999-10-06Fix for Unnamed_thm: Coq really uses this identifier.David Aspinall
1999-10-06More improvements/fixes for closing unfinished proofs.David Aspinall
Added proof-unnamed-theorem-name.
1999-10-06Made new command proof-cd to cd to the directory of the currentDavid Aspinall
buffer. Added a version of it to proof-activate-scripting-hook. Removed cd from initialization sequence. Changed prover specifics accordingly.
1999-10-06Fixed proof-showproof-commandDavid Aspinall
1999-10-06Fixed coq-interrupt-regexp.David Aspinall
1999-10-06Remove coq-Search function, now generic.David Aspinall
1999-10-01Renamed some configuration variables for uniformity, see CHANGES.David Aspinall
1999-10-01Disable proof-help-string, was set to an invalid command.David Aspinall
1999-09-24unified example with other proof assistants;Makarius Wenzel
1999-09-23Set proof-find-theorems-commandDavid Aspinall
1999-09-22proof-completed-regexp: match number 1 is response text;Makarius Wenzel
1999-09-13Failed attempt to prevent Coq from starting up with display of current ↵David Aspinall
directory.
1999-09-13Cleaned up example files so all demonstrate same theorem "conj_comms".David Aspinall
Would be nice to add more theorems to compare scripts in different systems.
1999-09-13Set proof-{qed,save}-commands.David Aspinall
1999-08-23Updated from Coq 6.3 distrib.David Aspinall
1999-08-23Updates suggested by Markus and Patrick for Coq 6.3.David Aspinall
1999-07-02fixed some regexp via proof-anchor-regexp;Makarius Wenzel
1999-06-30Missing parentheses added. Docstring fix.David Aspinall
1999-06-30last commit for 2.1Patrick Loiseleur
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 19:07:28 +0000