| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2013-01-28 | Update timestampes | David Aspinall | |
| 2013-01-21 | - implement proof-script insertion | Hendrik Tews | |
| 2013-01-20 | - implement retract from prooftree | Hendrik Tews | |
| 2013-01-17 | document latest changes | Hendrik Tews | |
| 2013-01-15 | - support bullets and braces in Prooftree | Hendrik Tews | |
| - prooftree protocol change to version 3 | |||
| 2012-11-14 | all-cpus option for coq-max-background-compilation-jobs | Hendrik Tews | |
| 2012-11-14 | update documentation | Hendrik Tews | |
| 2012-09-14 | no braces and bullets for prooftree | Hendrik Tews | |
| 2012-09-12 | treat #450 by requiring that proofs are started with Proof | Hendrik Tews | |
| 2012-08-14 | Add user option proof-next-command-insert-space. | David Aspinall | |
| 2012-06-19 | Completed documentation for file variables. | Pierre Courtieu | |
| 2012-05-29 | - erase invalid coq-load-path entry format '("dir") | Hendrik Tews | |
| - check if coq-load-path is well-formed - update documentation | |||
| 2012-05-09 | fix typo + add one missing cvsignore | Hendrik Tews | |
| 2012-01-05 | Update variable docs. Use HOL Light instead of HOL98. | David Aspinall | |
| 2012-01-03 | Add News for Version 4.2 | David Aspinall | |
| 2012-01-03 | merge ProofTreeBranch into main trunk: | Hendrik Tews | |
| - add support for proof-tree displays (currently Coq only) - new file generic/proof-tree.el contains generic code - Coq specific code has been added to coq/coq.el Changes to existing Proof General functions: - proof-shell-exec-loop and proof-shell-filter-manage-output call proof-tree display functions, when the proof-tree display is on - proof-shell-exec-loop returns t if proof-action-list is empty _or_ contains only items for updating the proof-tree - proof-shell-should-be-silent returns nil when the proof-tree display is on - coq-last-prompt-info, coq-last-prompt-info-safe return as additional 4th element the name of the current proof | |||
| 2011-10-14 | Bump doc version numbers to 4.2pre. | David Aspinall | |
| 2011-10-03 | Update dates and versions | David Aspinall | |
| 2011-09-23 | fix coqdep warning treated as error (library occurring at | Hendrik Tews | |
| multiple places in load-path) | |||
| 2011-09-19 | fix doc for coq -R patch | Hendrik Tews | |
| 2011-09-19 | Several improvements: | David Aspinall | |
| - explain how to use prefix commands for electric terminator as well as C-q - update explanation of locked region and read only options - explain colouring of modeline Scripting indicator - improve document-centred explanation, giving short-cut commands first - correct several uses of main menu "Proof General" to "Proof-General" with hyphen | |||
| 2011-09-15 | -add support for -R and -I -as in coq-load-path | Hendrik Tews | |
| -improve documentation (and reorder stuff) | |||
| 2011-09-14 | Add another contributor. | David Aspinall | |
| 2011-09-09 | fix documentation error | Hendrik Tews | |
| 2011-08-23 | Update magic | David Aspinall | |
| 2011-07-05 | + fix documentation and one spelling error | Hendrik Tews | |
| 2011-06-10 | Update dates, magic. | David Aspinall | |
| 2011-05-12 | Update docstring magic | David Aspinall | |
| 2011-05-05 | Update dates. | David Aspinall | |
| 2011-05-05 | Restore scary front page image. Add credits. | David Aspinall | |
| 2011-04-26 | Update magic, tweak Makefile to make sure magic uses source .els | David Aspinall | |
| 2011-04-13 | Add proof-output-tooltips option to turn off output highlighting for people ↵ | David Aspinall | |
| who read or edit by waving mouse at text | |||
| 2011-04-12 | typo | David Aspinall | |
| 2011-02-14 | put coq compilation feature into coq settings menu | Hendrik Tews | |
| 2011-02-02 | - properly display compilation error messages and enable M-x | Hendrik Tews | |
| next-error (as far as possible) | |||
| 2011-01-28 | - use low-level compilation interface for external coq | Hendrik Tews | |
| compilation with our own customization variables | |||
| 2011-01-28 | - mark new coq specific variables as safe | Hendrik Tews | |
| - hint on per-directory local variables | |||
| 2011-01-26 | - more info on the elements of proof-action-list; the COMMANDS | Hendrik Tews | |
| list in it should be concatenated with (mapconcat 'identity COMMANDS " "), which is not the case proof-shell-insert. | |||
| 2011-01-26 | - fix 1 second problem | Hendrik Tews | |
| - add limitations in the docs | |||
| 2011-01-24 | Add News for 4.1 | David Aspinall | |
| 2011-01-23 | Documentation updates | David Aspinall | |
| 2011-01-19 | Update date stamps | David Aspinall | |
| 2011-01-19 | - improved doc nodes Using file variables and Locking Ancestors | Hendrik Tews | |
| 2011-01-18 | - implemented coq-lock-ancestors as described in the docs already | Hendrik Tews | |
| 2011-01-18 | - fix broken external compilation | Hendrik Tews | |
| - fix quitting during compilation - substitute "compile" for "recompile" - added documentation | |||
| 2011-01-12 | Tweak text wrt http://proofgeneral.inf.ed.ac.uk/trac/ticket/355 | David Aspinall | |
| 2010-10-11 | Whitespace | David Aspinall | |
| 2010-10-11 | Add Adam Megacz to credits | David Aspinall | |
| 2010-10-10 | Cleanups. | David Aspinall | |
| 2010-10-10 | Update documenation of mouse bindings. | David Aspinall | |
| Clean up documentation of holes a bit. Remove some dead comments. | |||
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |