diff --git a/docs/editor.md b/docs/editor.md index bce31d0d25acbf05899cebdbf4803d28903d25c0..d59d4a550f267e949e03650f49447c213bcb98cf 100644 --- a/docs/editor.md +++ b/docs/editor.md @@ -134,14 +134,16 @@ To solve some of these indentation errors you can add the following line to your initialisation file: ``` (setq coq-smie-user-tokens - '(("∗" . "*") - ("-∗" . "->") - ("∗-∗" . "<->") - ("==∗" . "->") - ("⊢" . "->") - ("⊣⊢" . "<->") - ("⋅" . "*") - (":>" . ":="))) + '(("∗" . "*") + ("-∗" . "->") + ("∗-∗" . "<->") + ("==∗" . "->") + ("⊢" . "->") + ("⊣⊢" . "<->") + ("⋅" . "*") + (":>" . ":=") + ("by" . "now") + ("forall" . "now"))) ``` This will let the indentation strategy treat the Iris symbols (e.g. `-∗`) similar to the closely related Coq symbols (e.g. `->`).