diff --git a/docs/editor.md b/docs/editor.md
index d59d4a550f267e949e03650f49447c213bcb98cf..0933ff1903f952b755e84122f37c5ccdebaf9014 100644
--- a/docs/editor.md
+++ b/docs/editor.md
@@ -134,19 +134,48 @@ 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")))
+   '(("," . ":=")
+	("âˆ—" . "->")
+	("-âˆ—" . "->")
+	("âˆ—-âˆ—" . "->")
+	("==âˆ—" . "->")
+	("=âˆ—" . "->") 			;; Hack to match ={E1,E2}=âˆ—
+	("|==>" . ":=")
+	("âŠ¢" . "->")
+	("âŠ£âŠ¢" . "->")
+	("â†”" . "->")
+	("â†" . "<-")
+	("â†’" . "->")
+	("=" . "->")
+	("==" . "->")
+	("/\\" . "->")
+	("â‹…" . "->")
+	(":>" . ":=")
+	("by" . "now")
+	("forall" . "now")              ;; NB: this breaks current âˆ€ indentation.
+   ))
 ```
 This will let the indentation strategy treat the Iris symbols (e.g. `-âˆ—`) similar to the
 closely related Coq symbols (e.g. `->`).
+Note that `->` is used in many places, as its indentation behaviour is:
+```
+  P ->
+  Q
+```
+This is the indentation behaviour is what we want, e.g. for `âˆ—`:
+```
+  P âˆ—
+  Q
+```
+Note that this configuration has some caveats.
+Notably, the change to `forall` (which gives good behavior to e.g.
+`iInduction xs as [|x xs IHxs] forall (ys).`), now gives the following indentation
+behavior to universal quantification:
+```
+  âˆ€ x,
+  P x
+```
+This is not what we want; the second line should be indented by 2 spaces.
 
 ## CoqIDE 8.9 and earlier on Linux (ibus-m17n)