diff --git a/user/config/nvim/default.nix b/user/config/nvim/default.nix
index 4bee627..4d3915d 100644
--- a/user/config/nvim/default.nix
+++ b/user/config/nvim/default.nix
@@ -24,6 +24,7 @@
       bufferline-nvim
       nvim-colorizer-lua
       lazydev-nvim
+      Coqtail
       neorg
       (pkgs.vimUtils.buildVimPlugin {
         pname = "undotree";
@@ -46,7 +47,7 @@
       lua-language-server
     ];
     withRuby = false;
-    withPython3 = false;
+    withPython3 = true;
     withNodeJs = false;
   };
   xdg.configFile."nvim/init.lua".text = "require('init')";
diff --git a/user/config/nvim/lua/u/bindings.lua b/user/config/nvim/lua/u/bindings.lua
index 23d6ae9..832b1d9 100644
--- a/user/config/nvim/lua/u/bindings.lua
+++ b/user/config/nvim/lua/u/bindings.lua
@@ -10,3 +10,7 @@ map('n', '<leader>h', '<cmd>sp<cr>', {desc = "split [H]orizontal"})
 map('n', 'q:', '<nop>')
 map('n', '<leader>cd', vim.diagnostic.open_float, {desc = "[C]ode [D]iagnostic"})
 map('n', 'x', '"_x')
+map('n', '<c-a-j>', '<cmd>CoqNext<cr>')
+map('n', '<c-a-k>', '<cmd>CoqUndo<cr>')
+map('i', '<c-a-j>', '<cmd>CoqNext<cr>')
+map('i', '<c-a-k>', '<cmd>CoqUndo<cr>')