diff options
| author | Stefan Monnier | 2011-06-07 19:54:47 +0000 |
|---|---|---|
| committer | Stefan Monnier | 2011-06-07 19:54:47 +0000 |
| commit | d5b6bc3e78b4c89f41bd39469f7c6d936e391b97 (patch) | |
| tree | 5ecc4de8ed5652b1e640c81dff846d236721c3e5 /generic/proof-script.el | |
| parent | 3b3312870122a97db8a3be56fc065a50f715b8c9 (diff) | |
2011-06-07 Stefan Monnier <monnier@iro.umontreal.ca>
* 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".
Diffstat (limited to 'generic/proof-script.el')
0 files changed, 0 insertions, 0 deletions