Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Remove pointer to closed ticket | David Aspinall | 2011-06-22 |
| | |||
* | Set version tag for new release. | David Aspinall | 2011-06-22 |
| | |||
* | Set version tag for new release. | David Aspinall | 2011-06-22 |
| | |||
* | Removed { and } as command terminators for now. | Pierre Courtieu | 2011-06-19 |
| | | | | Fixes #412. | ||
* | oops, undo last commit. | Pierre Courtieu | 2011-06-17 |
| | |||
* | Fix mais le find-father ne marche pas encore. | Pierre Courtieu | 2011-06-17 |
| | |||
* | * coq.el: Fix up a few comment conventions; Improve SMIE indentation. | Stefan Monnier | 2011-06-11 |
| | | | | | | | | | (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, ..". | ||
* | Version bump | David Aspinall | 2011-06-10 |
| | |||
* | Set version tag for new release. | David Aspinall | 2011-06-10 |
| | |||
* | *** empty log message *** | David Aspinall | 2011-06-10 |
| | |||
* | Set version tag for new release. | David Aspinall | 2011-06-10 |
| | |||
* | Unplug smie cindentation code for this release. | Pierre Courtieu | 2011-06-10 |
| | |||
* | Fix trac #410. | Pierre Courtieu | 2011-06-10 |
| | |||
* | Deleted file | David Aspinall | 2011-06-10 |
| | |||
* | Update dates, magic. | David Aspinall | 2011-06-10 |
| | |||
* | Change linebreaks as Hendrik would like, not wiki formatted(!) | David Aspinall | 2011-06-09 |
| | |||
* | Add etc/coq/parsingcheck-410.v to executed files | David Aspinall | 2011-06-09 |
| | |||
* | parsing check from Trac #410 | David Aspinall | 2011-06-09 |
| | |||
* | Set version tag for new release. | David Aspinall | 2011-06-09 |
| | |||
* | Fix compile errors (seems to be code duplication between coq.el and coq-indent) | David Aspinall | 2011-06-09 |
| | |||
* | Update | David Aspinall | 2011-06-09 |
| | |||
* | Add autoload. | David Aspinall | 2011-06-09 |
| | |||
* | Added one indentation example. | Pierre Courtieu | 2011-06-08 |
| | |||
* | - fix for #408: Only use the buffer name in | Hendrik Tews | 2011-06-08 |
| | | | | | coq-compile-response-buffer - fix typo elsewhere | ||
* | 2011-06-07 Stefan Monnier <monnier@iro.umontreal.ca> | Stefan Monnier | 2011-06-07 |
| | | | | | | | | | | | | | * 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". | ||
* | Set version tag for new release. | David Aspinall | 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 | 2011-06-07 |
| | | | | | | | | | | | | | | | | * 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. | ||
* | Summary: coq-smie: Do not assume all "." are terminators. Handle "Programs". | Stefan Monnier | 2011-06-06 |
| | | | | | | (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. | ||
* | Record of bug report sent | David Aspinall | 2011-06-06 |
| | |||
* | *** empty log message *** | David Aspinall | 2011-06-06 |
| | |||
* | Updated the old code for indentation, in case Stefan cannot finish the | Pierre Courtieu | 2011-06-04 |
| | | | | | | | 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. | ||
* | Cleaning some keyboard shortcuts, applying patch from Erik Martin-Dorel. | Pierre Courtieu | 2011-06-04 |
| | |||
* | coq-init-compile-response-buffer: handle killed buffer (Trac #408) | David Aspinall | 2011-06-03 |
| | |||
* | proof-undo-and-delete-last-successful-command: obey spec (Trac #407) | David Aspinall | 2011-06-03 |
| | |||
* | Set version tag for new release. | David Aspinall | 2011-06-01 |
| | |||
* | Some small fixes in indentation for coq. | Pierre Courtieu | 2011-05-31 |
| | |||
* | Added indentation for BeginSubProof/EndSubProof. | Pierre Courtieu | 2011-05-31 |
| | | | | + added some tactics syntax. | ||
* | Set version tag for new release. | David Aspinall | 2011-05-30 |
| | |||
* | Trac#403: wait for retraction to complete before returning, to | David Aspinall | 2011-05-30 |
| | | | | avoid hitting read only error in calling command. | ||
* | ensure (integerp proof-segment-up-to-cache-end), fixes Trac #404 | David Aspinall | 2011-05-27 |
| | |||
* | Set version tag for new release. | David Aspinall | 2011-05-27 |
| | |||
* | proof-retract-before-change: fix Trac #403 (at least partially) by | David Aspinall | 2011-05-26 |
| | | | | | removing restriction during automatic retraction so proof-retract-until-point behaves correctly. | ||
* | - two fixes for coq-debug-auto-compilation | Hendrik Tews | 2011-05-25 |
| | |||
* | - minor changes: clean personal todo list + adjust test case description | Hendrik Tews | 2011-05-20 |
| | |||
* | Fixed #394. There is a bug with kfont-lock-keywords. The workaround is | Pierre Courtieu | 2011-05-17 |
| | | | | to change the order in which keywords appear. TO FIX. | ||
* | Set version tag for new release. | David Aspinall | 2011-05-16 |
| | |||
* | Update autogenerated files | David Aspinall | 2011-05-16 |
| | |||
* | Update docstrings | David Aspinall | 2011-05-16 |
| | |||
* | Patch for Trac#400. | David Aspinall | 2011-05-16 |
| |