diff --git a/docs/editor.md b/docs/editor.md
index 9318a2efd44e4fd34180f1f128aa1a2e7ad4aec6..40edd49c0ab1ea3798c4ecf4c4aa56999e3da4e3 100644
--- a/docs/editor.md
+++ b/docs/editor.md
@@ -347,3 +347,210 @@ Here is a `coqide.bindings` file for a variety of symbols used in Iris:
 \_v             áµ¥
 \_x             â‚“
 ```
+
+## Visual Studio Code
+
+### VSCoq setup
+
+The recommended extension as of December 2019 is [Maxime Dénès's
+VScoq](https://marketplace.visualstudio.com/items?itemName=maximedenes.vscoq).
+Press `Ctrl Shift P` or `Cmd Shift P` and then type "coq" to see the list of Coq
+commands and keyboard shortcuts.
+
+### Font setup
+
+To use unicode you need a font that supports all the symbols, such as [Fira
+Code](https://github.com/tonsky/FiraCode/wiki/Installing). Download and install
+the font, and in VS Code press `Cmd ,` or `Ctrl ,` to go to the settings, search
+for "font", and use "FiraCode-Retina" as the font-family and optionally enable
+ligatures.
+
+### Unicode input setup
+
+Install the [Generic input method
+extension](https://marketplace.visualstudio.com/items?itemName=mr-konn.generic-input-method).
+To insert a symbol, type the code for a symbol such as `\to` and then press
+`Space` or `Tab`. To enable Iris unicode input support, open your user settings,
+press `Cmd ,` or `Ctrl ,`, and type "generic-input-methods.input-methods", then
+click on "Edit in settings.json" and add the following:
+
+```
+  "generic-input-methods.input-methods": [
+        {
+            "name": "Iris Math",
+            "commandName": "text.math",
+            "languages": [
+                "coq"
+            ],
+            "triggers": [
+                "\\"
+            ],
+            "dictionary": [
+                // Standard LaTeX math notations
+                { "label": "forall", "body": "∀", "description": "∀" },
+                { "label": "exists", "body": "∃", "description": "∃" },
+                { "label": "lam", "body": "λ", "description": "λ" },
+                { "label": "not", "body": "¬", "description": "¬" },
+                { "label": "->", "body": "→", "description": "→" },
+                { "label": "<->", "body": "↔", "description": "↔" },
+                { "label": "<-", "body": "←", "description": "←" },
+                { "label": "==", "body": "≡", "description": "≡" },
+                { "label": "/==", "body": "≢", "description": "≢" },
+                { "label": "/=", "body": "≠", "description": "≠" },
+                { "label": "neq", "body": "≠", "description": "≠" },
+                { "label": "nequiv", "body": "≢", "description": "≢" },
+                { "label": "<=", "body": "≤", "description": "≤" },
+                { "label": "leq", "body": "≤", "description": "≤" },
+                { "label": "in", "body": "∈", "description": "∈" },
+                { "label": "notin", "body": "∉", "description": "∉" },
+                { "label": "cup", "body": "∪", "description": "∪" },
+                { "label": "cap", "body": "∩", "description": "∩" },
+                { "label": "setminus", "body": "∖", "description": "∖" },
+                { "label": "subset", "body": "⊂", "description": "⊂" },
+                { "label": "subseteq", "body": "⊆", "description": "⊆" },
+                { "label": "sqsubseteq", "body": "⊑", "description": "⊑" },
+                { "label": "sqsubseteq", "body": "⊑", "description": "⊑" },
+                { "label": "notsubseteq", "body": "⊈", "description": "⊈" },
+                { "label": "meet", "body": "⊓", "description": "⊓" },
+                { "label": "join", "body": "⊔", "description": "⊔" },
+                { "label": "top", "body": "⊤", "description": "⊤" },
+                { "label": "bottom", "body": "⊥", "description": "⊥" },
+                { "label": "vdash", "body": "⊢", "description": "⊢" },
+                { "label": "|-", "body": "⊢", "description": "⊢" },
+                { "label": "dashv", "body": "⊣", "description": "⊣" },
+                { "label": "Vdash", "body": "⊨", "description": "⊨" },
+                { "label": "infty", "body": "∞", "description": "∞" },
+                { "label": "comp", "body": "∘", "description": "∘" },
+                { "label": "prf", "body": "↾", "description": "↾" },
+                { "label": "bind", "body": "≫=", "description": "≫=" },
+                { "label": "mapsto", "body": "↦", "description": "↦" },
+                { "label": "hookrightarrow", "body": "↪", "description": "↪" },
+                { "label": "uparrow", "body": "↑", "description": "↑" },
+
+                // Iris specific
+                { "label": "fun", "body": "λ", "description": "λ" },
+                { "label": "mult", "body": "â‹…", "description": "â‹…" },
+                { "label": "ent", "body": "⊢", "description": "⊢" },
+                { "label": "valid", "body": "✓", "description": "✓" },
+                { "label": "diamond", "body": "â—‡", "description": "â—‡" },
+                { "label": "box", "body": "â–¡", "description": "â–¡" },
+                { "label": "bbox", "body": "â– ", "description": "â– " },
+                { "label": "later", "body": "â–·", "description": "â–·" },
+                { "label": "pred", "body": "φ", "description": "φ" },
+                { "label": "and", "body": "∧", "description": "∧" },
+                { "label": "or", "body": "∨", "description": "∨" },
+                { "label": "comp", "body": "∘", "description": "∘" },
+                { "label": "ccomp", "body": "â—Ž", "description": "â—Ž" },
+                { "label": "all", "body": "∀", "description": "∀" },
+                { "label": "ex", "body": "∃", "description": "∃" },
+                { "label": "to", "body": "→", "description": "→" },
+                { "label": "sep", "body": "∗", "description": "∗" },
+                { "label": "star", "body": "∗", "description": "∗" },
+                { "label": "lc", "body": "⌜", "description": "⌜" },
+                { "label": "rc", "body": "⌝", "description": "⌝" },
+                { "label": "Lc", "body": "⎡", "description": "⎡" },
+                { "label": "Rc", "body": "⎤", "description": "⎤" },
+                { "label": "empty", "body": "∅", "description": "∅" },
+                { "label": "Lam", "body": "Λ", "description": "Λ" },
+                { "label": "Sig", "body": "Σ", "description": "Σ" },
+                { "label": "-", "body": "∖", "description": "∖" },
+                { "label": "aa", "body": "●", "description": "●" },
+                { "label": "af", "body": "â—¯", "description": "â—¯" },
+                { "label": "auth", "body": "●", "description": "●" },
+                { "label": "frag", "body": "â—¯", "description": "â—¯" },
+                { "label": "iff", "body": "↔", "description": "↔" },
+                { "label": "gname", "body": "γ", "description": "γ" },
+                { "label": "incl", "body": "≼", "description": "≼" },
+                { "label": "latert", "body": "â–¶", "description": "â–¶" },
+                { "label": "update", "body": "⇝", "description": "⇝" },
+                { "label": "bind", "body": "≫=", "description": "≫=" },
+
+                // accents (for iLöb)
+                { "label": "\"o", "body": "ö", "description": "ö" },
+
+                // subscripts and superscripts
+                { "label": "^^+", "body": "⁺", "description": "⁺" },
+                { "label": "__+", "body": "â‚Š", "description": "â‚Š" },
+                { "label": "^^-", "body": "⁻", "description": "⁻" },
+                { "label": "__0", "body": "â‚€", "description": "â‚€" },
+                { "label": "__1", "body": "₁", "description": "₁" },
+                { "label": "__2", "body": "â‚‚", "description": "â‚‚" },
+                { "label": "__3", "body": "₃", "description": "₃" },
+                { "label": "__4", "body": "â‚„", "description": "â‚„" },
+                { "label": "__5", "body": "â‚…", "description": "â‚…" },
+                { "label": "__6", "body": "₆", "description": "₆" },
+                { "label": "__7", "body": "₇", "description": "₇" },
+                { "label": "__8", "body": "₈", "description": "₈" },
+                { "label": "__9", "body": "₉", "description": "₉" },
+                { "label": "__a", "body": "ₐ", "description": "ₐ" },
+                { "label": "__e", "body": "â‚‘", "description": "â‚‘" },
+                { "label": "__h", "body": "â‚•", "description": "â‚•" },
+                { "label": "__i", "body": "áµ¢", "description": "áµ¢" },
+                { "label": "__k", "body": "â‚–", "description": "â‚–" },
+                { "label": "__l", "body": "â‚—", "description": "â‚—" },
+                { "label": "__m", "body": "ₘ", "description": "ₘ" },
+                { "label": "__n", "body": "â‚™", "description": "â‚™" },
+                { "label": "__o", "body": "â‚’", "description": "â‚’" },
+                { "label": "__p", "body": "â‚š", "description": "â‚š" },
+                { "label": "__r", "body": "áµ£", "description": "áµ£" },
+                { "label": "__s", "body": "â‚›", "description": "â‚›" },
+                { "label": "__t", "body": "ₜ", "description": "ₜ" },
+                { "label": "__u", "body": "ᵤ", "description": "ᵤ" },
+                { "label": "__v", "body": "áµ¥", "description": "áµ¥" },
+                { "label": "__x", "body": "â‚“", "description": "â‚“" },
+
+                // Greek alphabet
+                { "label": "Alpha", "body": "Α", "description": "Α" },
+                { "label": "alpha", "body": "α", "description": "α" },
+                { "label": "Beta", "body": "Î’", "description": "Î’" },
+                { "label": "beta", "body": "β", "description": "β" },
+                { "label": "Gamma", "body": "Γ", "description": "Γ" },
+                { "label": "gamma", "body": "γ", "description": "γ" },
+                { "label": "Delta", "body": "Δ", "description": "Δ" },
+                { "label": "delta", "body": "δ", "description": "δ" },
+                { "label": "Epsilon", "body": "Ε", "description": "Ε" },
+                { "label": "epsilon", "body": "ε", "description": "ε" },
+                { "label": "Zeta", "body": "Ζ", "description": "Ζ" },
+                { "label": "zeta", "body": "ζ", "description": "ζ" },
+                { "label": "Eta", "body": "Η", "description": "Η" },
+                { "label": "eta", "body": "η", "description": "η" },
+                { "label": "Theta", "body": "Θ", "description": "Θ" },
+                { "label": "theta", "body": "θ", "description": "θ" },
+                { "label": "Iota", "body": "Ι", "description": "Ι" },
+                { "label": "iota", "body": "ι", "description": "ι" },
+                { "label": "Kappa", "body": "Κ", "description": "Κ" },
+                { "label": "kappa", "body": "κ", "description": "κ" },
+                { "label": "Lamda", "body": "Λ", "description": "Λ" },
+                { "label": "lamda", "body": "λ", "description": "λ" },
+                { "label": "Lambda", "body": "Λ", "description": "Λ" },
+                { "label": "lambda", "body": "λ", "description": "λ" },
+                { "label": "Mu", "body": "Μ", "description": "Μ" },
+                { "label": "mu", "body": "μ", "description": "μ" },
+                { "label": "Nu", "body": "Ν", "description": "Ν" },
+                { "label": "nu", "body": "ν", "description": "ν" },
+                { "label": "Xi", "body": "Ξ", "description": "Ξ" },
+                { "label": "xi", "body": "ξ", "description": "ξ" },
+                { "label": "Omicron", "body": "Ο", "description": "Ο" },
+                { "label": "omicron", "body": "ο", "description": "ο" },
+                { "label": "Pi", "body": "Π", "description": "Π" },
+                { "label": "pi", "body": "Ï€", "description": "Ï€" },
+                { "label": "Rho", "body": "Ρ", "description": "Ρ" },
+                { "label": "rho", "body": "ρ", "description": "ρ" },
+                { "label": "Sigma", "body": "Σ", "description": "Σ" },
+                { "label": "sigma", "body": "σ", "description": "σ" },
+                { "label": "Tau", "body": "Τ", "description": "Τ" },
+                { "label": "tau", "body": "Ï„", "description": "Ï„" },
+                { "label": "Upsilon", "body": "Î¥", "description": "Î¥" },
+                { "label": "upsilon", "body": "Ï…", "description": "Ï…" },
+                { "label": "Phi", "body": "Φ", "description": "Φ" },
+                { "label": "phi", "body": "φ", "description": "φ" },
+                { "label": "Chi", "body": "Χ", "description": "Χ" },
+                { "label": "chi", "body": "χ", "description": "χ" },
+                { "label": "Psi", "body": "Ψ", "description": "Ψ" },
+                { "label": "psi", "body": "ψ", "description": "ψ" },
+                { "label": "Omega", "body": "Ω", "description": "Ω" },
+                { "label": "omega", "body": "ω", "description": "ω" }
+            ]
+        }
+    ]
+```