| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Added an option about that in proof-config.
To check: I adapted proof-treee regrexp accordingly.
|
|
|
|
It is the only way I found to display informativemessage appearing
*before* the goal.
|
|
|
|
|
|
|
|
(coq-smie-backward-token): Don't burp at EOB.
(coq-smie-rules): Indent top-level ":" like ":=".
|
|
|
|
(coq-mode-config): Use it.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
file and directory name were not adapted to where the current file is
inside the directory structure. Now the absolute names are build.
|
|
are other uses of "where (declaring notation for records that I did no
test).
|
|
indented by default).
|
|
|
|
|
|
|
|
"=>" most of the time.
|
|
|
|
|
|
Not using "b o f" token anymore.
|
|
capture any operator and give it a (configurable?) precedence.
|
|
end of command, except if exactly <dot><dot>
|
|
Nasty bug due to smie fallback to backward-sexp when finding an
unknown token, namely the token "", which happens when reaching the
bof. Had to add a specific token for b o f.
|
|
|
