Merged requested to merge jules/iris:vscode-editor-docs into master
Added VS code to editor.md:
- Which extension to use for Coq.
- How to get a good unicode font that supports all the Iris symbols.
- Which extension to use for unicode input.
- A configuration file to configure unicode input for Iris (e.g. \later). Commands copied from those for CoqIDE..