| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2011-04-26 | Fix compile | David Aspinall | |
| 2011-04-26 | Fix so that make test.coq runs successfully. | David Aspinall | |
| 2011-04-26 | Clean up some defcustom docstrings (remove *'s) | David Aspinall | |
| 2011-04-15 | * fix coq-show-first-goal changing the current buffer | Hendrik Tews | |
| 2011-04-15 | * fix overwriting setq coq-prog-name before loading Proof General | Hendrik Tews | |
| * more complete callback listing in proof-action list doc | |||
| 2011-04-06 | * disable file safe when switching to new buffers for coq | Hendrik Tews | |
| 2011-03-14 | - change to proof-restart-buffers for unlocking ancestors | Hendrik Tews | |
| - improve internal docs for unlocking | |||
| 2011-02-28 | - fixed XXX'es in coq.el | Hendrik Tews | |
| 2011-02-28 | - adjust coq-ask-insert-coq-prog-name and doc in coq-local-vars-doc | Hendrik Tews | |
| 2011-02-18 | - deleted old coq multiple file stuff | Hendrik Tews | |
| 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-31 | Old debug setting | David Aspinall | |
| 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-28 | Clean coq goals buffer when backing to a non-proof state, otherwise | Pierre Courtieu | |
| the old goal was still displayed (and therefore the old number of goals too). Fixes trac #386. | |||
| 2011-01-26 | Add autotest-start with debug for now | David Aspinall | |
| 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-26 | - fix problem description | Hendrik Tews | |
| 2011-01-25 | - unlock files when retracting a Require command (implemented via | Hendrik Tews | |
| a span-delete-action and the 'coq-locked-ancestors property in the spans of Require commands) | |||
| 2011-01-25 | Remove proof-shell-wait that causes deadlock with new multiple-file code. | David Aspinall | |
| 2011-01-21 | - use time-less-p | Hendrik Tews | |
| - delete previous-head, simplify loop - coq 8.2 compatibility - describe bug for killing completely asserted active buffers in coq/ex/test-cases/retract-completely-asserted | |||
| 2011-01-19 | - switch off automatic compilation for coq to not surprise users | Hendrik Tews | |
| too much | |||
| 2011-01-18 | - fixed stale load path problem with killing the proof shell in | Hendrik Tews | |
| the deactivation-hook | |||
| 2011-01-18 | - implemented coq-lock-ancestors as described in the docs already | Hendrik Tews | |
| 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 | 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 | - more coq test cases (some with surprising and embarrassing bugs) | Hendrik Tews | |
| 2011-01-14 | Update dates and versions | 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 | |||
| 2010-11-25 | Fix compile problem with smie code on Emacs <=23.3 | 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-10-22 | Fixed a bug with utf8 error highlighting in coq 8.3 (bugs with 8.2 | Pierre Courtieu | |
| but nevermind). | |||
| 2010-10-10 | Add some more tokens for making pretty pictures | David Aspinall | |
| 2010-10-10 | coq-find-and-forget: Allow undoing prover processed regions | David Aspinall | |
| (i.e. files locked by Require). Some progress towards #363, and at least stops an ugly type error when a Require'd file is retracted. | |||
| 2010-10-10 | coq-generic-expression: fix this to match symbols, not merely words. | David Aspinall | |
| Otherwise we only see first word of symbols using underscores! | |||
| 2010-10-04 | Fixes in strings/comments from Erik Martin-Dorel | David Aspinall | |
| 2010-10-04 | coq-insert-solve-tactic: added (credit:Erik Martin-Dorel, patch from trac ↵ | David Aspinall | |
| #357). Docstring cleanups. | |||
| 2010-10-01 | Rename span-add-self-removing-span | David Aspinall | |
| 2010-10-01 | coq-highlight-error: use span-add-self-removing-span (highlight and removal ↵ | David Aspinall | |
| in background) | |||
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |