diff --git a/docs/coq_latex.snippets b/docs/coq_latex.snippets
new file mode 100644
index 0000000000000000000000000000000000000000..758b3a99ece4dd572d56f56a1889c2a3650d8eaa
--- /dev/null
+++ b/docs/coq_latex.snippets
@@ -0,0 +1,524 @@
+snippet \forall "" i
+∀
+endsnippet
+snippet \exists "" i
+∃
+endsnippet
+snippet \lam "" i
+λ
+endsnippet
+snippet \not "" i
+¬
+endsnippet
+snippet \lor "" i
+∨
+endsnippet
+snippet \land "" i
+∧
+endsnippet
+snippet \/ "" i
+∨
+endsnippet
+snippet /\ "" i
+∧
+endsnippet
+snippet \rightarrow "" i
+→
+endsnippet
+snippet \implies "" i
+→
+endsnippet
+snippet -> "" i
+→
+endsnippet
+snippet \iff "" i
+↔
+endsnippet
+snippet <-> "" i
+↔
+endsnippet
+snippet \<- "" i
+←
+endsnippet
+snippet \cong "" i
+≡
+endsnippet
+snippet \== "" i
+≡
+endsnippet
+snippet \/== "" i
+≢
+endsnippet
+snippet \neq "" i
+≠
+endsnippet
+snippet /= "" i
+≠
+endsnippet
+snippet \less "" i
+≤
+endsnippet
+snippet \le "" i
+≤
+endsnippet
+snippet <= "" i
+≤
+endsnippet
+snippet \in "" i
+∈
+endsnippet
+snippet \notin "" i
+∉
+endsnippet
+snippet \cup "" i
+∪
+endsnippet
+snippet \cap "" i
+∩
+endsnippet
+snippet \setminus "" i
+∖
+endsnippet
+snippet \subset "" i
+⊂
+endsnippet
+snippet \subseteq "" i
+⊆
+endsnippet
+snippet \sqsubseteq "" i
+⊑
+endsnippet
+snippet \sqsubseteq "" i
+⊑
+endsnippet
+snippet \notsubseteq "" i
+⊈
+endsnippet
+snippet \meet "" i
+⊓
+endsnippet
+snippet \join "" i
+⊔
+endsnippet
+snippet \true "" i
+⊤
+endsnippet
+snippet \top "" i
+⊤
+endsnippet
+snippet \false "" i
+⊥
+endsnippet
+snippet \bottom "" i
+⊥
+endsnippet
+snippet \vdash "" i
+⊢
+endsnippet
+snippet \dashv "" i
+⊣
+endsnippet
+snippet \vDash "" i
+⊨
+endsnippet
+snippet \Vdash
+⊩
+endsnippet
+snippet \infty "" i
+∞
+endsnippet
+snippet \comp "" i
+∘
+endsnippet
+snippet \prf "" i
+↾
+endsnippet
+snippet \bind "" i
+≫=
+endsnippet
+snippet \mapsto "" i
+↦
+endsnippet
+snippet \hookrightarrow "" i
+↪
+endsnippet
+snippet \up "" i
+↑
+endsnippet
+snippet \uparrow "" i
+↑
+endsnippet
+
+snippet \fun "" i
+λ
+endsnippet
+snippet \mult "" i
+â‹…
+endsnippet
+snippet \ent "" i
+⊢
+endsnippet
+snippet \valid "" i
+✓
+endsnippet
+snippet \diamond "" i
+â—‡
+endsnippet
+snippet \box "" i
+â–¡
+endsnippet
+snippet \bbox "" i
+â– 
+endsnippet
+snippet \eval "" i
+â–·
+endsnippet
+snippet \rhd "" i
+â–·
+endsnippet
+snippet \later "" i
+â–·
+endsnippet
+snippet \pred "" i
+φ
+endsnippet
+snippet \and "" i
+∧
+endsnippet
+snippet \or "" i
+∨
+endsnippet
+snippet \circ "" i
+∘
+endsnippet
+snippet \comp "" i
+∘
+endsnippet
+snippet \ccomp "" i
+â—Ž
+endsnippet
+snippet \pound "" i
+£
+endsnippet
+snippet \all "" i
+∀
+endsnippet
+snippet \ex "" i
+∃
+endsnippet
+snippet \to "" i
+→
+endsnippet
+snippet \ast "" i
+∗
+endsnippet
+snippet \sep "" i
+∗
+endsnippet
+snippet \ulc "" i
+⌜
+endsnippet
+snippet \urc "" i
+⌝
+endsnippet
+snippet \lc "" i
+⌜
+endsnippet
+snippet \rc "" i
+⌝
+endsnippet
+snippet \Lc "" i
+⎡
+endsnippet
+snippet \Rc "" i
+⎤
+endsnippet
+snippet \varnothing "" i
+∅
+endsnippet
+snippet \empty "" i
+∅
+endsnippet
+snippet \Lam "" i
+Λ
+endsnippet
+snippet \Sig "" i
+Σ
+endsnippet
+snippet \- "" i
+∖
+endsnippet
+snippet \aa "" i
+●
+endsnippet
+snippet \af "" i
+â—¯
+endsnippet
+snippet \auth "" i
+●
+endsnippet
+snippet \frag "" i
+â—¯
+endsnippet
+snippet \iff "" i
+↔
+endsnippet
+snippet \gname "" i
+γ
+endsnippet
+snippet \incl "" i
+≼
+endsnippet
+snippet \latert "" i
+â–¶
+endsnippet
+snippet \update "" i
+⇝
+endsnippet
+snippet \bind "" i
+≫=
+endsnippet
+
+
+snippet ^^+ "" i
+⁺
+endsnippet
+snippet __+ "" i
+â‚Š
+endsnippet
+snippet ^^- "" i
+⁻
+endsnippet
+snippet __0 "" i
+â‚€
+endsnippet
+snippet __1 "" i
+₁
+endsnippet
+snippet __2 "" i
+â‚‚
+endsnippet
+snippet __3 "" i
+₃
+endsnippet
+snippet __4 "" i
+â‚„
+endsnippet
+snippet __5 "" i
+â‚…
+endsnippet
+snippet __6 "" i
+₆
+endsnippet
+snippet __7 "" i
+₇
+endsnippet
+snippet __8 "" i
+₈
+endsnippet
+snippet __9 "" i
+₉
+endsnippet
+
+snippet __a "" i
+ₐ
+endsnippet
+snippet __e "" i
+â‚‘
+endsnippet
+snippet __h "" i
+â‚•
+endsnippet
+snippet __i "" i
+áµ¢
+endsnippet
+snippet __k "" i
+â‚–
+endsnippet
+snippet __l "" i
+â‚—
+endsnippet
+snippet __m "" i
+ₘ
+endsnippet
+snippet __n "" i
+â‚™
+endsnippet
+snippet __o "" i
+â‚’
+endsnippet
+snippet __p "" i
+â‚š
+endsnippet
+snippet __r "" i
+áµ£
+endsnippet
+snippet __s "" i
+â‚›
+endsnippet
+snippet __t "" i
+ₜ
+endsnippet
+snippet __u "" i
+ᵤ
+endsnippet
+snippet __v "" i
+áµ¥
+endsnippet
+snippet __x "" i
+â‚“
+endsnippet
+
+snippet \Alpha "" i
+Α
+endsnippet
+snippet \alpha "" i
+α
+endsnippet
+snippet \Beta "" i
+Î’
+endsnippet
+snippet \beta "" i
+β
+endsnippet
+snippet \Gamma "" i
+Γ
+endsnippet
+snippet \gamma "" i
+γ
+endsnippet
+snippet \Delta "" i
+Δ
+endsnippet
+snippet \delta "" i
+δ
+endsnippet
+snippet \Epsilon "" i
+Ε
+endsnippet
+snippet \epsilon "" i
+ε
+endsnippet
+snippet \Zeta "" i
+Ζ
+endsnippet
+snippet \zeta "" i
+ζ
+endsnippet
+snippet \Eta "" i
+Η
+endsnippet
+snippet \eta "" i
+η
+endsnippet
+snippet \Theta "" i
+Θ
+endsnippet
+snippet \theta "" i
+θ
+endsnippet
+snippet \Iota "" i
+Ι
+endsnippet
+snippet \iota "" i
+ι
+endsnippet
+snippet \Kappa "" i
+Κ
+endsnippet
+snippet \kappa "" i
+κ
+endsnippet
+snippet \Lamda "" i
+Λ
+endsnippet
+snippet \lamda "" i
+λ
+endsnippet
+snippet \Lambda "" i
+Λ
+endsnippet
+snippet \lambda "" i
+λ
+endsnippet
+snippet \Mu "" i
+Μ
+endsnippet
+snippet \mu "" i
+μ
+endsnippet
+snippet \Nu "" i
+Ν
+endsnippet
+snippet \nu "" i
+ν
+endsnippet
+snippet \Xi "" i
+Ξ
+endsnippet
+snippet \xi "" i
+ξ
+endsnippet
+snippet \Omicron "" i
+Ο
+endsnippet
+snippet \omicron "" i
+ο
+endsnippet
+snippet \Pi "" i
+Π
+endsnippet
+snippet \pi "" i
+Ï€
+endsnippet
+snippet \Rho "" i
+Ρ
+endsnippet
+snippet \rho "" i
+ρ
+endsnippet
+snippet \Sigma "" i
+Σ
+endsnippet
+snippet \sigma "" i
+σ
+endsnippet
+snippet \Tau "" i
+Τ
+endsnippet
+snippet \tau "" i
+Ï„
+endsnippet
+snippet \Upsilon "" i
+Î¥
+endsnippet
+snippet \upsilon "" i
+Ï…
+endsnippet
+snippet \Phi "" i
+Φ
+endsnippet
+snippet \phi "" i
+Ï•
+endsnippet
+snippet \varphi "" i
+φ
+endsnippet
+snippet \Chi "" i
+Χ
+endsnippet
+snippet \chi "" i
+χ
+endsnippet
+snippet \Psi "" i
+Ψ
+endsnippet
+snippet \psi "" i
+ψ
+endsnippet
+snippet \Omega "" i
+Ω
+endsnippet
+snippet \omega "" i
+ω
+endsnippet
diff --git a/docs/editor.md b/docs/editor.md
index 92ff9a3ee30dfc3ced2fb82fa44959e199cf717d..b4f8ac2d889db6f486174f2d6b4bfc06501a09b7 100644
--- a/docs/editor.md
+++ b/docs/editor.md
@@ -696,532 +696,6 @@ Install it with your favorite plugin manager, and register a completion key in y
 ```
 let g:UltiSnipsExpandTrigger="<c-l>"
 ```
-To insert a unicode character, type its trigger word, such as `\forall`, and then press `<c-l>` while still in insert mode.
+To insert a unicode character, type its trigger word, such as `\forall` or `->`, and then press `<c-l>` while still in insert mode.
 
-To register most common unicode characters, put the following file either at `~/.vim/UltiSnips/coq_latex.snippets` or `~/.config/nvim/UltiSnips/coq_latex.snippets`, depending on your preferred variant of Vim:
-```
-snippet \forall "" i
-∀
-endsnippet
-snippet \exists "" i
-∃
-endsnippet
-snippet \lam "" i
-λ
-endsnippet
-snippet \not "" i
-¬
-endsnippet
-snippet \lor "" i
-∨
-endsnippet
-snippet \land "" i
-∧
-endsnippet
-snippet \/ "" i
-∨
-endsnippet
-snippet /\ "" i
-∧
-endsnippet
-snippet \rightarrow "" i
-→
-endsnippet
-snippet \implies "" i
-→
-endsnippet
-snippet -> "" i
-→
-endsnippet
-snippet \iff "" i
-↔
-endsnippet
-snippet <-> "" i
-↔
-endsnippet
-snippet \<- "" i
-←
-endsnippet
-snippet \cong "" i
-≡
-endsnippet
-snippet \== "" i
-≡
-endsnippet
-snippet \/== "" i
-≢
-endsnippet
-snippet \neq "" i
-≠
-endsnippet
-snippet /= "" i
-≠
-endsnippet
-snippet \less "" i
-≤
-endsnippet
-snippet \le "" i
-≤
-endsnippet
-snippet <= "" i
-≤
-endsnippet
-snippet \in "" i
-∈
-endsnippet
-snippet \notin "" i
-∉
-endsnippet
-snippet \cup "" i
-∪
-endsnippet
-snippet \cap "" i
-∩
-endsnippet
-snippet \setminus "" i
-∖
-endsnippet
-snippet \subset "" i
-⊂
-endsnippet
-snippet \subseteq "" i
-⊆
-endsnippet
-snippet \sqsubseteq "" i
-⊑
-endsnippet
-snippet \sqsubseteq "" i
-⊑
-endsnippet
-snippet \notsubseteq "" i
-⊈
-endsnippet
-snippet \meet "" i
-⊓
-endsnippet
-snippet \join "" i
-⊔
-endsnippet
-snippet \true "" i
-⊤
-endsnippet
-snippet \top "" i
-⊤
-endsnippet
-snippet \false "" i
-⊥
-endsnippet
-snippet \bottom "" i
-⊥
-endsnippet
-snippet \vdash "" i
-⊢
-endsnippet
-snippet \dashv "" i
-⊣
-endsnippet
-snippet \vDash "" i
-⊨
-endsnippet
-snippet \Vdash
-⊩
-endsnippet
-snippet \infty "" i
-∞
-endsnippet
-snippet \comp "" i
-∘
-endsnippet
-snippet \prf "" i
-↾
-endsnippet
-snippet \bind "" i
-≫=
-endsnippet
-snippet \mapsto "" i
-↦
-endsnippet
-snippet \hookrightarrow "" i
-↪
-endsnippet
-snippet \up "" i
-↑
-endsnippet
-snippet \uparrow "" i
-↑
-endsnippet
-
-snippet \fun "" i
-λ
-endsnippet
-snippet \mult "" i
-â‹…
-endsnippet
-snippet \ent "" i
-⊢
-endsnippet
-snippet \valid "" i
-✓
-endsnippet
-snippet \diamond "" i
-â—‡
-endsnippet
-snippet \box "" i
-â–¡
-endsnippet
-snippet \bbox "" i
-â– 
-endsnippet
-snippet \eval "" i
-â–·
-endsnippet
-snippet \rhd "" i
-â–·
-endsnippet
-snippet \later "" i
-â–·
-endsnippet
-snippet \pred "" i
-φ
-endsnippet
-snippet \and "" i
-∧
-endsnippet
-snippet \or "" i
-∨
-endsnippet
-snippet \circ "" i
-∘
-endsnippet
-snippet \comp "" i
-∘
-endsnippet
-snippet \ccomp "" i
-â—Ž
-endsnippet
-snippet \pound "" i
-£
-endsnippet
-snippet \all "" i
-∀
-endsnippet
-snippet \ex "" i
-∃
-endsnippet
-snippet \to "" i
-→
-endsnippet
-snippet \ast "" i
-∗
-endsnippet
-snippet \sep "" i
-∗
-endsnippet
-snippet \ulc "" i
-⌜
-endsnippet
-snippet \urc "" i
-⌝
-endsnippet
-snippet \lc "" i
-⌜
-endsnippet
-snippet \rc "" i
-⌝
-endsnippet
-snippet \Lc "" i
-⎡
-endsnippet
-snippet \Rc "" i
-⎤
-endsnippet
-snippet \varnothing "" i
-∅
-endsnippet
-snippet \empty "" i
-∅
-endsnippet
-snippet \Lam "" i
-Λ
-endsnippet
-snippet \Sig "" i
-Σ
-endsnippet
-snippet \- "" i
-∖
-endsnippet
-snippet \aa "" i
-●
-endsnippet
-snippet \af "" i
-â—¯
-endsnippet
-snippet \auth "" i
-●
-endsnippet
-snippet \frag "" i
-â—¯
-endsnippet
-snippet \iff "" i
-↔
-endsnippet
-snippet \gname "" i
-γ
-endsnippet
-snippet \incl "" i
-≼
-endsnippet
-snippet \latert "" i
-â–¶
-endsnippet
-snippet \update "" i
-⇝
-endsnippet
-snippet \bind "" i
-≫=
-endsnippet
-
-
-snippet ^^+ "" i
-⁺
-endsnippet
-snippet __+ "" i
-â‚Š
-endsnippet
-snippet ^^- "" i
-⁻
-endsnippet
-snippet __0 "" i
-â‚€
-endsnippet
-snippet __1 "" i
-₁
-endsnippet
-snippet __2 "" i
-â‚‚
-endsnippet
-snippet __3 "" i
-₃
-endsnippet
-snippet __4 "" i
-â‚„
-endsnippet
-snippet __5 "" i
-â‚…
-endsnippet
-snippet __6 "" i
-₆
-endsnippet
-snippet __7 "" i
-₇
-endsnippet
-snippet __8 "" i
-₈
-endsnippet
-snippet __9 "" i
-₉
-endsnippet
-
-snippet __a "" i
-ₐ
-endsnippet
-snippet __e "" i
-â‚‘
-endsnippet
-snippet __h "" i
-â‚•
-endsnippet
-snippet __i "" i
-áµ¢
-endsnippet
-snippet __k "" i
-â‚–
-endsnippet
-snippet __l "" i
-â‚—
-endsnippet
-snippet __m "" i
-ₘ
-endsnippet
-snippet __n "" i
-â‚™
-endsnippet
-snippet __o "" i
-â‚’
-endsnippet
-snippet __p "" i
-â‚š
-endsnippet
-snippet __r "" i
-áµ£
-endsnippet
-snippet __s "" i
-â‚›
-endsnippet
-snippet __t "" i
-ₜ
-endsnippet
-snippet __u "" i
-ᵤ
-endsnippet
-snippet __v "" i
-áµ¥
-endsnippet
-snippet __x "" i
-â‚“
-endsnippet
-
-snippet \Alpha "" i
-Α
-endsnippet
-snippet \alpha "" i
-α
-endsnippet
-snippet \Beta "" i
-Î’
-endsnippet
-snippet \beta "" i
-β
-endsnippet
-snippet \Gamma "" i
-Γ
-endsnippet
-snippet \gamma "" i
-γ
-endsnippet
-snippet \Delta "" i
-Δ
-endsnippet
-snippet \delta "" i
-δ
-endsnippet
-snippet \Epsilon "" i
-Ε
-endsnippet
-snippet \epsilon "" i
-ε
-endsnippet
-snippet \Zeta "" i
-Ζ
-endsnippet
-snippet \zeta "" i
-ζ
-endsnippet
-snippet \Eta "" i
-Η
-endsnippet
-snippet \eta "" i
-η
-endsnippet
-snippet \Theta "" i
-Θ
-endsnippet
-snippet \theta "" i
-θ
-endsnippet
-snippet \Iota "" i
-Ι
-endsnippet
-snippet \iota "" i
-ι
-endsnippet
-snippet \Kappa "" i
-Κ
-endsnippet
-snippet \kappa "" i
-κ
-endsnippet
-snippet \Lamda "" i
-Λ
-endsnippet
-snippet \lamda "" i
-λ
-endsnippet
-snippet \Lambda "" i
-Λ
-endsnippet
-snippet \lambda "" i
-λ
-endsnippet
-snippet \Mu "" i
-Μ
-endsnippet
-snippet \mu "" i
-μ
-endsnippet
-snippet \Nu "" i
-Ν
-endsnippet
-snippet \nu "" i
-ν
-endsnippet
-snippet \Xi "" i
-Ξ
-endsnippet
-snippet \xi "" i
-ξ
-endsnippet
-snippet \Omicron "" i
-Ο
-endsnippet
-snippet \omicron "" i
-ο
-endsnippet
-snippet \Pi "" i
-Π
-endsnippet
-snippet \pi "" i
-Ï€
-endsnippet
-snippet \Rho "" i
-Ρ
-endsnippet
-snippet \rho "" i
-ρ
-endsnippet
-snippet \Sigma "" i
-Σ
-endsnippet
-snippet \sigma "" i
-σ
-endsnippet
-snippet \Tau "" i
-Τ
-endsnippet
-snippet \tau "" i
-Ï„
-endsnippet
-snippet \Upsilon "" i
-Î¥
-endsnippet
-snippet \upsilon "" i
-Ï…
-endsnippet
-snippet \Phi "" i
-Φ
-endsnippet
-snippet \phi "" i
-Ï•
-endsnippet
-snippet \varphi "" i
-φ
-endsnippet
-snippet \Chi "" i
-Χ
-endsnippet
-snippet \chi "" i
-χ
-endsnippet
-snippet \Psi "" i
-Ψ
-endsnippet
-snippet \psi "" i
-ψ
-endsnippet
-snippet \Omega "" i
-Ω
-endsnippet
-snippet \omega "" i
-ω
-endsnippet
-```
+To register most common unicode characters, put [this file](/docs/coq_latex.snippets) either at `~/.vim/UltiSnips/coq_latex.snippets` or `~/.config/nvim/UltiSnips/coq_latex.snippets`, depending on your preferred variant of Vim.