Skip to content

Commit 7723c16

Browse files
committed
Remove unused plugin settings
These were removed upstream, and Johannes also reported that they apparently didn't do anything.
1 parent c28d973 commit 7723c16

2 files changed

Lines changed: 0 additions & 9 deletions

File tree

.devcontainer/devcontainer.json

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -15,13 +15,10 @@
1515
"**/*.vok": true,
1616
"**/.*.cache": true
1717
},
18-
"coq.loadCoqProject": true,
19-
"coq.coqProjectRoot": ".",
2018
"[coq]": {
2119
"editor.tabSize": 2,
2220
"editor.insertSpaces": true
2321
},
24-
"vscoq.path": "/home/coq/.opam/4.14.2+flambda/bin/vscoqtop",
2522
"editor.unicodeHighlight.ambiguousCharacters": false,
2623
"generic-input-methods.input-methods": [
2724
{

README.md

Lines changed: 0 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -29,12 +29,6 @@ See [here](https://marketplace.visualstudio.com/items?itemName=ms-vscode-remote.
2929
### Running `Dev Containers: Reopen in Container` cannot find the container
3030
Make sure you copied the `.devcontainer` folder to your project's root folder and that it includes the `devcontainer.json` file.
3131

32-
### `Cannot find a physical path bound to logical path X with prefix Y` when importing a file
33-
* Make sure that the Rocq files have been compiled. Run `make` to compile the project files.
34-
* If the `_CoqProject` files are not located in the project root folder you need to either
35-
* Move the files to the root project folder
36-
* Or add the line `"coq.coqProjectRoot": "PATH_TO_COQPROJECT"` (in `.devcontainer/devcontainer.json` to point to the directory where `_CoqProject` is located. Restarting the docker container is required after this step.
37-
3832
### Problems on Apple Silicon
3933
Run `docker pull --platform linux/amd64 <the docker link>` to force the `x86` version of the Docker container to be installed.
4034
This should then trick Docker into using some kind of emulation, and the software should work natively.

0 commit comments

Comments
 (0)