aboutsummaryrefslogtreecommitdiff
path: root/FAQ.md
diff options
context:
space:
mode:
authorPierre Courtieu2020-01-14 15:38:50 +0100
committerPierre Courtieu2020-01-19 15:46:46 +0100
commit054bed9c667344024077202cc4ca2fd4e77c4842 (patch)
treee56f4ebd28bd9a30bf11f2740da2a76ea5632422 /FAQ.md
parentbee3f802ada921fb8988edb96a8b41429f7c622c (diff)
Generic monadic indentation + specifically ext-lib / Compcert + doc.
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.
Diffstat (limited to 'FAQ.md')
0 files changed, 0 insertions, 0 deletions