diff --git a/CHANGES.md b/CHANGES.md
index 3ccb5fe2..0b2961a8 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -153,6 +153,8 @@
    and info messages appear as diagnostics
  - Display the continous/on-request checking mode in the status bar,
    allow to change it by clicking on it (@ejgallego, #721)
+ - Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
+   #611)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------
diff --git a/etc/doc/USER_MANUAL.md b/etc/doc/USER_MANUAL.md
index 18234e72..4fc5288d 100644
--- a/etc/doc/USER_MANUAL.md
+++ b/etc/doc/USER_MANUAL.md
@@ -98,7 +98,18 @@ A setting to have `coq-lsp` check documents continuously exists.
 You can tell the server to free up memory with the "Coq LSP: Free
 memory" command.
 
-## Advanced: Multiple workspaces
+## Advanced: Multiple Workspaces
+
+`coq-lsp` does support projects that combine multiple Coq project
+roots in a single workspace. That way, one can develop on several
+distinct Coq developments seamlessly.
+
+To enable this, use the "Add Folder" option in VSCode, where each root
+must be a folder containing a `_CoqProject` file.
+
+Check the example at
+[../../examples/multiple_workspaces/](../../examples/multiple_workspaces/)
+to see it in action!
 
 ## Interrupting coq-lsp
 
diff --git a/examples/multiple_workspaces/README.md b/examples/multiple_workspaces/README.md
new file mode 100644
index 00000000..58ebebfc
--- /dev/null
+++ b/examples/multiple_workspaces/README.md
@@ -0,0 +1,42 @@
+# Multiple workspaces setup
+
+## How to run it:
+
+Try to load the `example.code-workspace` file in VSCode.
+
+You may need to compile the right `.vo` files for the imports to
+work. You can do that with the `Save VO command`; as of now, `coq-lsp`
+will require you do this before opening the depending files.
+
+`coq-lsp` will take care of this automatically in the next version,
+including the auto-update. You can also do:
+
+```sh
+$ coqc -R bar bar bar/barx.y
+$ coqc -R foo foo foo/foox.y
+```
+
+## `coq-lsp` workspace documentation
+
+One can add multiple folders or roots to a workspace — for instance
+via the "Add Folder to Workspace" command (or
+[alternatives](https://code.visualstudio.com/docs/editor/multi-root-workspaces#_adding-folders)).
+
+For each workspace added to a project, `coq-lsp` will try to configure
+it by searching for a `_CoqProject` file, then it will apply the
+options found there. In the near future, we will also detect
+`dune-project` files at the root too.
+
+`coq-lsp` does determine the workspace roots using the standard
+methods provided by the LSP protocol, in particular `wsFolders`,
+`rootURI`, and `rootPath` at initialiation, in this order; and by
+listening to the `workspace/didChangeWorkspaceFolders` notification
+after initialization.
+
+## Known problems
+
+When projects are using Coq plugins, `findlib` doesn't properly
+support having multiple roots in the same process. We are using a hack
+that seems to work (we reinitialize `findlib`), however the hack is
+very fragile; we should improve `findlib` upstream to support our use
+case.
diff --git a/examples/multiple_workspaces/bar/_CoqProject b/examples/multiple_workspaces/bar/_CoqProject
new file mode 100644
index 00000000..475f78d8
--- /dev/null
+++ b/examples/multiple_workspaces/bar/_CoqProject
@@ -0,0 +1 @@
+-R . bar
diff --git a/examples/multiple_workspaces/bar/barx.v b/examples/multiple_workspaces/bar/barx.v
new file mode 100644
index 00000000..5fcaa519
--- /dev/null
+++ b/examples/multiple_workspaces/bar/barx.v
@@ -0,0 +1,3 @@
+Definition x := 3.
+
+Print x.
diff --git a/examples/multiple_workspaces/bar/bary.v b/examples/multiple_workspaces/bar/bary.v
new file mode 100644
index 00000000..d2fabedf
--- /dev/null
+++ b/examples/multiple_workspaces/bar/bary.v
@@ -0,0 +1,3 @@
+From bar Require Import barx.
+
+Print x.
diff --git a/examples/multiple_workspaces/example.code-workspace b/examples/multiple_workspaces/example.code-workspace
new file mode 100644
index 00000000..e72e6f59
--- /dev/null
+++ b/examples/multiple_workspaces/example.code-workspace
@@ -0,0 +1,27 @@
+{
+	"folders": [
+		{
+			"path": "bar"
+		},
+		{
+			"path": "foo"
+		}
+	],
+	"settings": {
+		"files.exclude": {
+			"**/*.vo": true,
+			"**/*.vok": true,
+			"**/*.vos": true,
+			"**/*.aux": true,
+			"**/*.glob": true,
+			"**/.git": true,
+			"**/.svn": true,
+			"**/.hg": true,
+			"**/CVS": true,
+			"**/.DS_Store": true,
+			"**/Thumbs.db": true,
+			"**/*.olean": true,
+			"out": false
+		}
+	}
+}
\ No newline at end of file
diff --git a/examples/multiple_workspaces/foo/_CoqProject b/examples/multiple_workspaces/foo/_CoqProject
new file mode 100644
index 00000000..35a0741d
--- /dev/null
+++ b/examples/multiple_workspaces/foo/_CoqProject
@@ -0,0 +1 @@
+-R . foo
diff --git a/examples/multiple_workspaces/foo/foox.v b/examples/multiple_workspaces/foo/foox.v
new file mode 100644
index 00000000..82ae5066
--- /dev/null
+++ b/examples/multiple_workspaces/foo/foox.v
@@ -0,0 +1,3 @@
+Definition x := 3.
+
+Print x.
\ No newline at end of file
diff --git a/examples/multiple_workspaces/foo/fooy.v b/examples/multiple_workspaces/foo/fooy.v
new file mode 100644
index 00000000..c80500f5
--- /dev/null
+++ b/examples/multiple_workspaces/foo/fooy.v
@@ -0,0 +1,3 @@
+From foo Require Import foox.
+
+Print x.