Update INSTALL.md

INSTALL.md

@@ -39,6 +39,11 @@ Here are the instructions:
 - Wait for VSCode to download a 1.28 GB archive that extracts to about 6 GB, on
   our system this takes about 2 min.
 - Wait for VSCode to compile the code of the plugin, this takes about 30s.
+  The last line of the terminal output should be
+  ```
+  make[1]: Leaving directory '/workspaces/trocq'
+  ```
+  before you can actually skip to the next section.
 
 ### Via Nix (recommended only for nix/nixos users)
 
@@ -90,6 +95,10 @@ goal generated by Trocq to replace the initial one. The process should be almost
 instantaneous on all the examples. Please note that on the first time a line is
 clicked in a file, the proof state can take a few seconds to update.
 
+If you have unexpected errors press "Ctrl-Shift-P" to get the command palette
+and type `Coq LSP: Restart the Coq Language Server` and enter to reload the
+Coq <-> VSCode communication.
+
 ### Example from the artifact paper
 
 In file `artifact_paper_example.v`, this amounts to putting the pointer on line