Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | coq-load-path docs: norec -> nonrec (#79) | Timothy Bourke | 2016-06-18 |
| | |||
* | Update license information for new logo | Clément Pit--Claudel | 2016-05-25 |
| | |||
* | Update PG's logo | Clément Pit--Claudel | 2016-05-24 |
| | | | | | | | The new art is a contribution of Yoshihiro Imai (http://proofcafe.org/~yoshihiro503/), first released at https://github.com/yoshihiro503/generaltan and kindly made available under the terms of the GPL. Many thanks! | ||
* | Update numbering flag passed to texi2html | Tej Chajed | 2016-02-10 |
| | | | | | | texi2html, as of version 1.80 (http://download-mirror.savannah.gnu.org/releases//texi2html/NEWS-1.80), uses -number-sections instead of -number for the flag name. | ||
* | A remark about project file in the documentation. | Pierre Courtieu | 2015-03-26 |
| | | | | | Saying that one -arg should be followed by only one option. For several options, put several -arg, ONE PER LINE. | ||
* | Update dates for release next month | David Aspinall | 2015-03-13 |
| | |||
* | Fix crossref broken by newline. Remove custom font | David Aspinall | 2015-01-05 |
| | |||
* | Added some information on coq project file in doc. | Pierre Courtieu | 2013-07-22 |
| | |||
* | Fix image name | David Aspinall | 2013-07-17 |
| | |||
* | fix ProofGeneral.texi for info | Hendrik Tews | 2013-07-17 |
| | |||
* | Updating pg documentation about new feature coq project file. | Pierre Courtieu | 2013-07-05 |
| | |||
* | rename ProofGeneral.{jpg,gif} into ProofGeneral-image.{jpg,gif} | Hendrik Tews | 2013-05-22 |
| | | | | to fix #472 | ||
* | Retire Serifa font usage | David Aspinall | 2013-05-22 |
| | |||
* | - update coq example | Hendrik Tews | 2013-05-14 |
| | | | | - minor changes in user manual | ||
* | add 4.3 news to user manual | Hendrik Tews | 2013-03-27 |
| | |||
* | Update timestampes | David Aspinall | 2013-01-28 |
| | |||
* | - implement proof-script insertion | Hendrik Tews | 2013-01-21 |
| | |||
* | - implement retract from prooftree | Hendrik Tews | 2013-01-20 |
| | |||
* | document latest changes | Hendrik Tews | 2013-01-17 |
| | |||
* | - support Grab Existential Variables for Prooftree | Hendrik Tews | 2013-01-17 |
| | | | | - protocol change, but stay at version 3 | ||
* | removal of backup files (*~) moved to make distclean | Hendrik Tews | 2013-01-15 |
| | |||
* | - support bullets and braces in Prooftree | Hendrik Tews | 2013-01-15 |
| | | | | - prooftree protocol change to version 3 | ||
* | fix parallel overlapping calls of proof-shell-filter | Hendrik Tews | 2013-01-10 |
| | |||
* | all-cpus option for coq-max-background-compilation-jobs | Hendrik Tews | 2012-11-14 |
| | |||
* | update documentation | Hendrik Tews | 2012-11-14 |
| | |||
* | no braces and bullets for prooftree | Hendrik Tews | 2012-09-14 |
| | |||
* | treat #450 by requiring that proofs are started with Proof | Hendrik Tews | 2012-09-12 |
| | |||
* | Add user option proof-next-command-insert-space. | David Aspinall | 2012-08-14 |
| | |||
* | Completed documentation for file variables. | Pierre Courtieu | 2012-06-19 |
| | |||
* | - erase invalid coq-load-path entry format '("dir") | Hendrik Tews | 2012-05-29 |
| | | | | | - check if coq-load-path is well-formed - update documentation | ||
* | fix typo + add one missing cvsignore | Hendrik Tews | 2012-05-09 |
| | |||
* | Typo | David Aspinall | 2012-01-19 |
| | |||
* | Add documentation for proof-shell-trace-output-regexp (Trac #432) and | David Aspinall | 2012-01-10 |
| | | | | proof-shell-interactive-prompt-regexp (ref Trac #430) | ||
* | Update variable docs. Use HOL Light instead of HOL98. | David Aspinall | 2012-01-05 |
| | |||
* | Add News for Version 4.2 | David Aspinall | 2012-01-03 |
| | |||
* | Remove unused variable | David Aspinall | 2012-01-03 |
| | |||
* | merge ProofTreeBranch into main trunk: | Hendrik Tews | 2012-01-03 |
| | | | | | | | | | | | | | | | | - 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 | ||
* | Add web style sheet to doc output (work in progress) | David Aspinall | 2011-11-09 |
| | |||
* | Bump doc version numbers to 4.2pre. | David Aspinall | 2011-10-14 |
| | |||
* | Update dates and versions | David Aspinall | 2011-10-03 |
| | |||
* | fix coqdep warning treated as error (library occurring at | Hendrik Tews | 2011-09-23 |
| | | | | multiple places in load-path) | ||
* | fix doc for coq -R patch | Hendrik Tews | 2011-09-19 |
| | |||
* | Several improvements: | David Aspinall | 2011-09-19 |
| | | | | | | | | - 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 | ||
* | -add support for -R and -I -as in coq-load-path | Hendrik Tews | 2011-09-15 |
| | | | | -improve documentation (and reorder stuff) | ||
* | Add another contributor. | David Aspinall | 2011-09-14 |
| | |||
* | fix documentation error | Hendrik Tews | 2011-09-09 |
| | |||
* | Update magic | David Aspinall | 2011-08-23 |
| | |||
* | + fix documentation and one spelling error | Hendrik Tews | 2011-07-05 |
| | |||
* | Update dates, magic. | David Aspinall | 2011-06-10 |
| | |||
* | Update docstrings | David Aspinall | 2011-05-16 |
| |