| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2011-01-18 | Add multiple file test case | David Aspinall | |
| 2011-01-18 | Alternative fix to #382. | David Aspinall | |
| 2011-01-18 | set proof-auto-action-when-deactivating-scripting to 'retract, | David Aspinall | |
| to stop new multiple file handling for Coq interactive queries | |||
| 2011-01-18 | Localise compilation fix for dynamic scope of `queueitems\'. | David Aspinall | |
| 2011-01-18 | - fixed compilation errors | Hendrik Tews | |
| 2011-01-18 | - fix broken external compilation | Hendrik Tews | |
| - fix quitting during compilation - substitute "compile" for "recompile" - added documentation | |||
| 2011-01-18 | Removing a debugging message. | Pierre Courtieu | |
| 2011-01-18 | Set version tag for new release. | David Aspinall | |
| 2011-01-18 | Fix trac 382 by not setting save-abbrevs. | Pierre Courtieu | |
| 2011-01-17 | fix problems in test cases | Hendrik Tews | |
| coq/ex/test-cases/multiple-files-single-dir and multiple-files-multiple-dir | |||
| 2011-01-14 | set a non-temporary email address | Hendrik Tews | |
| 2011-01-14 | - more coq test cases (some with surprising and embarrassing bugs) | Hendrik Tews | |
| 2011-01-14 | Update dates and versions | David Aspinall | |
| 2011-01-14 | Add new CVS users to DEVELOPERS list. | David Aspinall | |
| 2011-01-14 | - move proof-no-fully-processed-buffer to generic/proof-config | Hendrik Tews | |
| - add documentation for it - add a test case demonstrating it in coq/ex/test-cases/retract-completely-asserted | |||
| 2011-01-14 | - simple backward compatible change to invoke a function to | Hendrik Tews | |
| compute the command line arguments for a proof assistant | |||
| 2011-01-14 | - Remove nonfunctional Add LoadPath code. | Hendrik Tews | |
| - Use coqdep now to map the required module to a file name. "Require Arith." works now, but coqdep fails on "Require Arith.Le.". - Remove the coq-internal-load-path hash and all related function. Coq's load path logic is too complicated to reimplement that in ProofGeneral | |||
| 2011-01-12 | Add preliminary support for multiple files for coq. | Hendrik Tews | |
| The following points are implemented already: - recompile either via an external command (make) or let ProofGeneral handle everything internally - complete dependency tracking and recompilation for coq files in internal mode - support for extending the LoadPath: does almost work, even if specified file-locally - move back to clean state if recompilation fails There are the following known problems: - coq-load-path extensions are not retracted - fails on partially qualified library names | |||
| 2011-01-12 | Tweak text wrt http://proofgeneral.inf.ed.ac.uk/trac/ticket/355 | David Aspinall | |
| 2011-01-12 | Set version tag for new release. | David Aspinall | |
| 2011-01-12 | Remove comment | David Aspinall | |
| 2011-01-12 | Type-check on integer settings | David Aspinall | |
| 2011-01-12 | Fix quoting in 'float patch. | David Aspinall | |
| 2011-01-11 | Add additional support for pgipfloat type | David Aspinall | |
| 2011-01-11 | 'float -> 'number | David Aspinall | |
| 2011-01-11 | defpacustom: support for 'float type | David Aspinall | |
| 2010-12-16 | Set version tag for new release. | David Aspinall | |
| 2010-12-16 | Patch to add pgipfloat type. | David Aspinall | |
| 2010-12-15 | Updated | David Aspinall | |
| 2010-12-10 | Updated compatibility | David Aspinall | |
| 2010-12-10 | Set version tag for new release. | David Aspinall | |
| 2010-12-10 | Update date | David Aspinall | |
| 2010-12-10 | Add note about short list | David Aspinall | |
| 2010-12-08 | some attempts to indent 'notepad' 'begin' ... 'end' like a proof body; | Makarius Wenzel | |
| 2010-11-25 | Fix compile problem with smie code on Emacs <=23.3 | David Aspinall | |
| 2010-11-25 | Set version tag for new release. | David Aspinall | |
| 2010-11-15 | Summary: New indentation code using SMIE | Stefan Monnier | |
| * coq/coq.el (coq-build-prog-args): Avoid meaningless \- escape sequence. (coq-use-smie): New custom var. (coq-smie-grammar): New var. (coq-smie-rules): New function. (coq-guess-or-ask-for-string): Use use-region-p. (coq-mode-config): Use smie-setup if available. * lib/proof-compat.el (use-region-p): Provide fallback definition. | |||
| 2010-11-09 | Address http://proofgeneral.inf.ed.ac.uk/trac/ticket/379 | David Aspinall | |
| 2010-11-03 | Updated. | David Aspinall | |
| 2010-11-03 | Set version tag for new release. | David Aspinall | |
| 2010-10-22 | Fixed a bug with utf8 error highlighting in coq 8.3 (bugs with 8.2 | Pierre Courtieu | |
| but nevermind). | |||
| 2010-10-13 | Update for config changes. | David Aspinall | |
| 2010-10-11 | proof-debug: fiddle with warning levels to make *PG Debug* buffer appear, ↵ | David Aspinall | |
| set it in help mode. | |||
| 2010-10-11 | proof-segment-up-to-using-cache: improve attempt | David Aspinall | |
| 2010-10-11 | Set version tag for new release. | David Aspinall | |
| 2010-10-11 | proof-use-parser-cache=t default | David Aspinall | |
| 2010-10-11 | Whitespace | David Aspinall | |
| 2010-10-11 | Use parser cache by default. | David Aspinall | |
| 2010-10-11 | Add Adam Megacz to credits | David Aspinall | |
| 2010-10-11 | Updated | David Aspinall | |
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |