diff --git a/docs/editor.md b/docs/editor.md index 438252da9d8602f9aa88560b31154f9c4f950e35..bce31d0d25acbf05899cebdbf4803d28903d25c0 100644 --- a/docs/editor.md +++ b/docs/editor.md @@ -125,6 +125,27 @@ results in a decent choice for the symbols used in Iris: (set-fontset-font t nil (font-spec :name "Symbola")) ``` +### Automated Indentation + +The default indentation configuration of company-coq is not compatible with the Iris syntax. +As a result, automatic indentation will indent lines incorrectly. + +To solve some of these indentation errors you can add the following line to your Emacs +initialisation file: +``` +(setq coq-smie-user-tokens + '(("∗" . "*") + ("-∗" . "->") + ("∗-∗" . "<->") + ("==∗" . "->") + ("⊢" . "->") + ("⊣⊢" . "<->") + ("⋅" . "*") + (":>" . ":="))) +``` +This will let the indentation strategy treat the Iris symbols (e.g. `-∗`) similar to the +closely related Coq symbols (e.g. `->`). + ## CoqIDE 8.9 and earlier on Linux (ibus-m17n) On Linux with old versions of CoqIDE you can use the Intelligent