aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc/PG-adapting.texi
Commit message (Collapse)AuthorAge
* Update timestampesGravatar David Aspinall2013-01-28
|
* - implement proof-script insertionGravatar Hendrik Tews2013-01-21
|
* - implement retract from prooftreeGravatar Hendrik Tews2013-01-20
|
* - support Grab Existential Variables for ProoftreeGravatar Hendrik Tews2013-01-17
| | | | - protocol change, but stay at version 3
* fix parallel overlapping calls of proof-shell-filterGravatar Hendrik Tews2013-01-10
|
* update documentationGravatar Hendrik Tews2012-11-14
|
* - erase invalid coq-load-path entry format '("dir")Gravatar Hendrik Tews2012-05-29
| | | | | - check if coq-load-path is well-formed - update documentation
* TypoGravatar David Aspinall2012-01-19
|
* Add documentation for proof-shell-trace-output-regexp (Trac #432) andGravatar David Aspinall2012-01-10
| | | | proof-shell-interactive-prompt-regexp (ref Trac #430)
* Update variable docs. Use HOL Light instead of HOL98.Gravatar David Aspinall2012-01-05
|
* merge ProofTreeBranch into main trunk:Gravatar Hendrik Tews2012-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
* Bump doc version numbers to 4.2pre.Gravatar David Aspinall2011-10-14
|
* Update dates and versionsGravatar David Aspinall2011-10-03
|
* -add support for -R and -I -as in coq-load-pathGravatar Hendrik Tews2011-09-15
| | | | -improve documentation (and reorder stuff)
* Update dates, magic.Gravatar David Aspinall2011-06-10
|
* Update docstringsGravatar David Aspinall2011-05-16
|
* Update docstring magicGravatar David Aspinall2011-05-12
|
* Restore front page scary image. Update datesGravatar David Aspinall2011-05-05
|
* - flushed proof-done-advancing-require-function andGravatar Hendrik Tews2011-05-05
| | | | | proof-shell-require-command-regexp - TAGS updated to really flush them
* Update magic, tweak Makefile to make sure magic uses source .elsGravatar David Aspinall2011-04-26
|
* - change to proof-restart-buffers for unlocking ancestorsGravatar Hendrik Tews2011-03-14
| | | | - improve internal docs for unlocking
* put coq compilation feature into coq settings menuGravatar Hendrik Tews2011-02-14
|
* - more info on the elements of proof-action-list; the COMMANDSGravatar Hendrik Tews2011-01-26
| | | | | list in it should be concatenated with (mapconcat 'identity COMMANDS " "), which is not the case proof-shell-insert.
* Documentation updatesGravatar David Aspinall2011-01-23
|
* Update date stampsGravatar David Aspinall2011-01-19
|
* - implemented coq-lock-ancestors as described in the docs alreadyGravatar Hendrik Tews2011-01-18
|
* - move proof-no-fully-processed-buffer to generic/proof-configGravatar Hendrik Tews2011-01-14
| | | | | | - add documentation for it - add a test case demonstrating it in coq/ex/test-cases/retract-completely-asserted
* Update magicGravatar David Aspinall2010-10-10
|
* Document query identifierGravatar David Aspinall2010-10-01
|
* Update magic, release datesGravatar David Aspinall2010-10-01
|
* Update magicGravatar David Aspinall2010-08-27
|
* Update to use @dircategory and @direntry for infoGravatar David Aspinall2010-08-23
|
* Fix menu/node order inside internal chapterGravatar David Aspinall2010-08-15
|
* Update magicGravatar David Aspinall2009-12-01
|
* Updates to internal function docsGravatar David Aspinall2009-11-29
|
* Remove function-menu as promisedGravatar David Aspinall2009-10-14
|
* Update magicGravatar David Aspinall2009-09-30
|
* Update docsGravatar David Aspinall2009-09-15
|
* Remove errant ^AGravatar David Aspinall2009-09-15
|
* More text about Unicode TokensGravatar David Aspinall2009-09-08
| | | | Remove proof-shell-abort-goal-regexp
* Update: mention scomint, remove old variables/functionsGravatar David Aspinall2009-09-06
|
* Remove proof-shell-prompt-pattern, no longer used.Gravatar David Aspinall2009-09-04
|
* Update versionsGravatar David Aspinall2009-08-31
|
* Clarify mode functions. Fix cross references to Elisp ref (not XEmacs Lispref)Gravatar David Aspinall2009-08-28
|
* Add recommendation for DejaVu fonts. Update magic.Gravatar David Aspinall2009-08-25
|
* proof-looking-at-syntactic-context: add doc. Update doc/names of proof ↵Gravatar David Aspinall2009-08-17
| | | | shell filter functions.
* Document document centric mechanism. Other updates and additions. Remove ↵Gravatar David Aspinall2009-08-07
| | | | experimental features.
* Updates for Isabelle2009, new electric terminator behaviour.Gravatar David Aspinall2009-05-26
|
* TweakGravatar David Aspinall2008-12-05
|
* Some minimal updates for 4.0preGravatar David Aspinall2008-12-05
|