| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2020-01-19 | Generic monadic indentation + specifically ext-lib / Compcert + doc. | Pierre Courtieu | |
| This a generalization of PR#451 proposed by @Chobbes. Since these syntax are not completely universal (and not builtin in coq), the idea is to make the syntax customizable, especially to make it possible to disable it. NOTE: to make the Compcert syntax supported I had to refine the smie lexer so that the ";" token was emitted as a fllback instead of "; tactic". NOTE2: I had to make the coq-user-token and coq-monadic-tokens be tested ON THE RESULT of smie-coq-backward-token. | |||
 |
index : proof-general | |
| Emacs plugins for proof management systems |
| aboutsummaryrefslogtreecommitdiff |