| 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.
|
|
display-buffer-alist infrastructure if available.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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).
|
