diff --git a/doc/vscode.rst b/doc/vscode.rst
index f67936484..bcc958b94 100644
--- a/doc/vscode.rst
+++ b/doc/vscode.rst
@@ -23,17 +23,27 @@ Make sure you have a `lambdapi.pkg <https://lambdapi.readthedocs.io/en/latest/mo
 
 Goals are visualised in a panel on the right side of the editor. You can
 navigate in proof with the following key-bindings:
-
--  ``Ctrl+Right``: go one step forward
--  ``Ctrl+Left``: go one step backward
--  ``Ctrl+Up``: go to the previous proof (or the beginning)
--  ``Ctrl+Down``: go to the next proof (or the end)
--  ``Ctrl+Enter``: go to the position of the cursor
--  ``Ctrl+Alt+c``: toggle cursor mode (proof highlight follows the
-   cursor or not)
--  ``Ctrl+Alt+w``: toggle follow mode (proof highlight is always
-   centered in the window when keybindings are pressed)
--  ``Shift+Alt+w``: center proof highlight in the current window
+***Linux and Windows***
+- ``Ctrl+Right``: go one step forward
+- ``Ctrl+Left``: go one step backward
+- ``Ctrl+Up``: go to the previous proof (or the beginning)
+- ``Ctrl+Down``: go to the next proof (or the end)
+- ``Ctrl+Enter``: go to the position of the cursor
+- ``Ctrl+Alt+c``: toggle cursor mode (proof highlight follows the cursor or not)
+- ``Ctrl+Alt+w``: toggle follow mode (proof highligsht is always centered in the window when keybindings are pressed)
+- ``Shift+Alt+w``: center proof highlight in the current window
+
+***Mac OS X***
+- ``Ctrl+fn+Right``: go one step forward
+- ``Ctrl+fn+Left``: go one step backward
+- ``Ctrl+Alt+Up``: go to the previous proof (or the beginning)
+- ``Ctrl+Alt+Down``: go to the next proof (or the end)
+- ``Ctrl+Enter``: go to the position of the cursor
+- ``Ctrl+Alt+c``: toggle cursor mode (proof highlight follows the cursor or not)
+- ``Ctrl+Alt+w``: toggle follow mode (proof highlight is always centered in the window when keybindings are pressed)
+- ``Shift+Alt+w``: center proof highlight in the current window
+
+Please note that these key-bindings can be changed in Code->Preferences->keyboard shortcuts (also reachable with Ctrl+K Ctrl+S or Command+K Command+S in Mac OS X).
 
 **Hover and go-to-definition**
 
diff --git a/editors/vscode/CHANGES.md b/editors/vscode/CHANGES.md
index a3afb4099..16c084b31 100644
--- a/editors/vscode/CHANGES.md
+++ b/editors/vscode/CHANGES.md
@@ -10,6 +10,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/).
 ### Fixed
 
 ### Changed
+- Changed the `go to the previous/next proof` commands shortcuts for Mac OS X operating system because previous ones are used by Mac OS.
 - When calling lambdapi to launch the lsp server from the Vscode extension, read the `lsp` argument from `package.json` instead of hard-coding it to allow using a custom command to launch the server especially in Windows as discussed in issue #1163 (Many thanks to Akihisa Yamada)
 
 ## [0.2.2]
diff --git a/editors/vscode/README.md b/editors/vscode/README.md
index 61694845a..429f45127 100644
--- a/editors/vscode/README.md
+++ b/editors/vscode/README.md
@@ -5,15 +5,28 @@ This extension provides support for the [Lambdapi](https://github.com/Deducteam/
 Goals are visualised in a panel on the right side of the editor.
 You can navigate in proof with the following key-bindings:
 
+***Linux and Windows***
 - ``Ctrl+Right``: go one step forward
 - ``Ctrl+Left``: go one step backward
 - ``Ctrl+Up``: go to the previous proof (or the beginning)
 - ``Ctrl+Down``: go to the next proof (or the end)
 - ``Ctrl+Enter``: go to the position of the cursor
 - ``Ctrl+Alt+c``: toggle cursor mode (proof highlight follows the cursor or not)
+- ``Ctrl+Alt+w``: toggle follow mode (proof highligsht is always centered in the window when keybindings are pressed)
+- ``Shift+Alt+w``: center proof highlight in the current window
+
+***Mac OS X***
+- ``Ctrl+fn+Right``: go one step forward
+- ``Ctrl+fn+Left``: go one step backward
+- ``Ctrl+Alt+Up``: go to the previous proof (or the beginning)
+- ``Ctrl+Alt+Down``: go to the next proof (or the end)
+- ``Ctrl+Enter``: go to the position of the cursor
+- ``Ctrl+Alt+c``: toggle cursor mode (proof highlight follows the cursor or not)
 - ``Ctrl+Alt+w``: toggle follow mode (proof highlight is always centered in the window when keybindings are pressed)
 - ``Shift+Alt+w``: center proof highlight in the current window
 
+Please note that these key-bindings can be changed in Code->Preferences->keyboard shortcuts (also reachable with Ctrl+K Ctrl+S or Command+K Command+S in Mac OS X).
+
 **Hover and go-to-definition**
 
 Hovering a token will display its type if available.
diff --git a/editors/vscode/package.json b/editors/vscode/package.json
index 292f324cf..a8f43f16a 100644
--- a/editors/vscode/package.json
+++ b/editors/vscode/package.json
@@ -145,12 +145,22 @@
       {
         "key": "ctrl+up",
         "command": "extension.lambdapi.pv",
-        "when": "editorTextFocus && editorLangId == lp"
+        "when": "editorTextFocus && editorLangId == lp && (isWindows || isLinux)"
       },
       {
         "key": "ctrl+down",
         "command": "extension.lambdapi.nx",
-        "when": "editorTextFocus && editorLangId == lp"
+        "when": "editorTextFocus && editorLangId == lp && (isWindows || isLinux)"
+      },
+      {
+        "key": "ctrl+alt+up",
+        "command": "extension.lambdapi.pv",
+        "when": "editorTextFocus && editorLangId == lp && isMac"
+      },
+      {
+        "key": "ctrl+alt+down",
+        "command": "extension.lambdapi.nx",
+        "when": "editorTextFocus && editorLangId == lp && isMac"
       }
     ],
     "snippets": [