| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2011-06-22 | Remove pointer to closed ticket | David Aspinall | |
| 2011-06-19 | Removed { and } as command terminators for now. | Pierre Courtieu | |
| Fixes #412. | |||
| 2011-06-17 | oops, undo last commit. | Pierre Courtieu | |
| 2011-06-17 | Fix mais le find-father ne marche pas encore. | Pierre Courtieu | |
| 2011-06-11 | * coq.el: Fix up a few comment conventions; Improve SMIE indentation. | Stefan Monnier | |
| (coq-smie-grammar): Use new special token "Proof End". (coq-smie-proof-end-tokens): New var. (coq-smie-forward-token, coq-smie-backward-token): Map proof end tokens to "Proof End", and map "(Next )Obligation" to "Proof". (coq-smie-rules): Indent after ;-tactical. Use "Proof End". Indent specially "Lemma x :forall, ..". | |||
| 2011-06-10 | Unplug smie cindentation code for this release. | Pierre Courtieu | |
| 2011-06-10 | Fix trac #410. | Pierre Courtieu | |
| 2011-06-09 | Add etc/coq/parsingcheck-410.v to executed files | David Aspinall | |
| 2011-06-09 | Fix compile errors (seems to be code duplication between coq.el and coq-indent) | David Aspinall | |
| 2011-06-08 | Added one indentation example. | Pierre Courtieu | |
| 2011-06-08 | - fix for #408: Only use the buffer name in | Hendrik Tews | |
| coq-compile-response-buffer - fix typo elsewhere | |||
| 2011-06-07 | 2011-06-07 Stefan Monnier <monnier@iro.umontreal.ca> | Stefan Monnier | |
| * coq/coq.el: Match Proof...Qed and fix ;-vs-| precedence. (coq-smie-grammar): Add ; and | tacticals. Rename decls => cmds. Add CoInductive, and Proof..Qed. (coq-smie-search-token-forward): Rename from coq-smie-search-token; make it more robust. (coq-smie-search-token-backward): New function. (coq-smie-forward-token, coq-smie-backward-token): Use it to distinguish Inductive's ":=" from other uses. (coq-smie-rules): Use smie-rule-separator for |. Add ugly hack for Qed without matching "Proof". | |||
| 2011-06-07 | Summary: * coq.el (coq-smie-backward-token): Fix typo in last change. | Stefan Monnier | |
| 2011-06-07 | Summary: coq-smie: improve indentation. | Stefan Monnier | |
| * coq.el (coq-smie-grammar): Add rules for {|...|}, Let, Record, Module..End, Section..End, and BeginSubproof..EndSubproof. (coq-smie-search-token): New function. (coq-smie-forward-token, coq-smie-backward-token): Recognize {| and |}. Distinguish Module definition from Module introduction. Merge "Module Type" and "Module". (coq-smie-rules): Refine list-intro. Improve indentation after "with". Add Function, Let and Record to the := case. Indent within Module..End and friends. Improve indentation of record def. Indent forall's body by 2. Better indent Lemmas. * coq-db.el (coq-build-abbrev-table-from-db): Mark those abbrevs as `system'. * coq-abbrev.el (coq-install-abbrevs): Don't bind save-abbrevs since it's not needed any more. | |||
| 2011-06-06 | Summary: coq-smie: Do not assume all "." are terminators. Handle "Programs". | Stefan Monnier | |
| (coq-smie-grammar): Add "Function" rule. (coq-smie-forward-token, coq-smie-backward-token): New functions. (coq-mode-config): Use them for the SMIE lexer. | |||
| 2011-06-04 | Updated the old code for indentation, in case Stefan cannot finish the | Pierre Courtieu | |
| new one for the release. Added also support for an experimental syntax modification: { .. } is a new syntax for Beginsubproof. ... EndSubproof. There a also few minor behavior changes. The code has changed a lot though. | |||
| 2011-06-04 | Cleaning some keyboard shortcuts, applying patch from Erik Martin-Dorel. | Pierre Courtieu | |
| 2011-06-03 | coq-init-compile-response-buffer: handle killed buffer (Trac #408) | David Aspinall | |
| 2011-05-31 | Some small fixes in indentation for coq. | Pierre Courtieu | |
| 2011-05-31 | Added indentation for BeginSubProof/EndSubProof. | Pierre Courtieu | |
| + added some tactics syntax. | |||
| 2011-05-25 | - two fixes for coq-debug-auto-compilation | Hendrik Tews | |
| 2011-05-20 | - minor changes: clean personal todo list + adjust test case description | Hendrik Tews | |
| 2011-05-17 | Fixed #394. There is a bug with kfont-lock-keywords. The workaround is | Pierre Courtieu | |
| to change the order in which keywords appear. TO FIX. | |||
| 2011-05-12 | - add test coq/ex/test-cases/change-ancestor for the | Hendrik Tews | |
| change-ancestor bug | |||
| 2011-05-06 | Checkdoc | David Aspinall | |
| 2011-05-05 | - flushed proof-done-advancing-require-function and | Hendrik Tews | |
| proof-shell-require-command-regexp - TAGS updated to really flush them | |||
| 2011-04-27 | update Hendrik's personal issue list | Hendrik Tews | |
| 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 | |||
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |