diff --git a/plugins/completion/coq.nix b/plugins/completion/coq.nix
new file mode 100644
index 00000000..ab135743
--- /dev/null
+++ b/plugins/completion/coq.nix
@@ -0,0 +1,47 @@
+{ pkgs, lib, config, ... }:
+with lib;
+let
+  cfg = config.programs.nixvim.plugins.coq-nvim;
+  helpers = import ../helpers.nix { lib = lib; };
+  plugins = import ../plugin-defs.nix { inherit pkgs; };
+
+in {
+  options = {
+    programs.nixvim.plugins.coq-nvim = {
+      enable = mkEnableOption "Enable coq-nvim";
+
+      installArtifacts = mkEnableOption "Install coq-artifacts";
+
+      autoStart = mkOption {
+        type = with types; nullOr (oneOf [bool (enum ["shut-up"])]);
+        default = null;
+        description = "Auto-start or shut up";
+      };
+
+      recommendedKeymaps = mkOption {
+        type = with types; nullOr bool;
+        default = null;
+        description = "Use the recommended keymaps";
+      };
+    };
+  };
+  config = let
+    settings = {
+      auto_start = cfg.autoStart;
+      "keymap.recommended" = cfg.recommendedKeymaps;
+    };
+  in mkIf cfg.enable {
+    programs.nixvim = {
+      extraPlugins = [
+        plugins.coq-nvim
+      ] ++ optional cfg.installArtifacts plugins.coq-artifacts;
+      plugins.lsp = {
+        preConfig = ''
+          vim.g.coq_settings = ${helpers.toLuaObject settings}
+          local coq = require 'coq'
+        '';
+        setupWrappers = [(s: ''coq.lsp_ensure_capabilities(${s})'')];
+      };
+    };
+  };
+}
diff --git a/plugins/default.nix b/plugins/default.nix
index 8b142199..947a7ef2 100644
--- a/plugins/default.nix
+++ b/plugins/default.nix
@@ -9,6 +9,8 @@
     ./colorschemes/onedark.nix
     ./colorschemes/tokyonight.nix
 
+    ./completion/coq.nix
+
     ./git/fugitive.nix
     ./git/gitgutter.nix
 
diff --git a/plugins/nvim-lsp/default.nix b/plugins/nvim-lsp/default.nix
index 7d1ec650..fba24feb 100644
--- a/plugins/nvim-lsp/default.nix
+++ b/plugins/nvim-lsp/default.nix
@@ -40,33 +40,49 @@ in
         default = "";
       };
 
-      capabilities = mkOption {
+      setupWrappers = mkOption {
+        type = with types; listOf (functionTo str);
+        description = "Code to be run to wrap the setup args. Takes in an argument containing the previous results, and returns a new string of code.";
+        default = [];
+      };
+
+      preConfig = mkOption {
         type = types.lines;
-        description = "A lua function defining the capabilities of a new LSP buffer.";
+        description = "Code to be run before loading the LSP. Useful for requiring plugins";
         default = "";
       };
     };
   };
 
-  config = mkIf cfg.enable {
+  config = let
+    runWrappers = wrappers: s:
+    if wrappers == [] then s
+    else (head wrappers) (runWrappers (tail wrappers) s);
+  in mkIf cfg.enable {
     programs.nixvim = {
       extraPlugins = [ pkgs.vimPlugins.nvim-lspconfig ];
 
       # Enable all LSP servers
       extraConfigLua = ''
         -- LSP {{{
-        local __lspServers = ${helpers.toLuaObject cfg.enabledServers}
-        local __lspOnAttach = function(client)
-          ${cfg.onAttach}
-        end
+        do
+          ${cfg.preConfig}
+          local __lspServers = ${helpers.toLuaObject cfg.enabledServers}
+          local __lspOnAttach = function(client)
+            ${cfg.onAttach}
+          end
 
-        for i,server in ipairs(__lspServers) do
-          if type(server) == "string" then
-            require('lspconfig')[server].setup {
-              on_attach = __lspOnAttach
-            }
-          else
-            require('lspconfig')[server.name].setup(server.extraOptions)
+          local __setup = ${runWrappers cfg.setupWrappers "{
+            on_attach = __lspOnAttach
+          }"}
+
+          for i,server in ipairs(__lspServers) do
+            if type(server) == "string" then
+              require('lspconfig')[server].setup(__setup)
+            else
+              local options = ${runWrappers cfg.setupWrappers "server.extraOptions"}
+              require('lspconfig')[server.name].setup(options)
+            end
           end
         end
         -- }}}
diff --git a/plugins/plugin-defs.nix b/plugins/plugin-defs.nix
index 204c376c..d6e9cda3 100644
--- a/plugins/plugin-defs.nix
+++ b/plugins/plugin-defs.nix
@@ -23,4 +23,65 @@
       sha256 = "1y3l2c7h8czhw0b5m25iyjdyy0p4nqk4a3bxv583m72hn4ac8rz9";
     };
   };
+  coq-nvim = pkgs.vimUtils.buildVimPlugin rec {
+    pname = "coq-nvim";
+    version = "2699492a1b8716c59ade7130dc354e53944b6a7f";
+    src = pkgs.fetchFromGitHub {
+      owner = "ms-jpq";
+      repo = "coq_nvim";
+      rev = version;
+      sha256 = "sha256-tjniIWe1V4vGuao5no+3YB9WtiNaMehEjffJyNpFgd8=";
+    };
+
+    passthru.python3Dependencies = ps: [
+      ps.pynvim
+      ps.pyyaml
+      (ps.buildPythonPackage rec {
+        pname = "pynvim_pp";
+        version = "01dc0f58d4e71a98c388e1f37bda3d1357089fa2";
+
+        src = pkgs.fetchFromGitHub {
+          owner = "ms-jpq";
+          repo = "pynvim_pp";
+          rev = version;
+          sha256 = "sha256-/m4Paw6AvDzTMWWCWpPnrdI4gsjIDSJPvGCMV7ufbEA=";
+        };
+
+        propagatedBuildInputs = [ pkgs.python3Packages.pynvim ];
+      })
+      (ps.buildPythonPackage rec {
+        pname = "std2";
+        version = "48bb39b69ed631ef64eed6123443484133fd20fc";
+
+        doCheck = false;
+
+        src = pkgs.fetchFromGitHub {
+          owner = "ms-jpq";
+          repo = "std2";
+          rev = version;
+          sha256 = "sha256-nMwNAq15zyf9ORhFGo0sawQukOygYoVWtT7jH68MIkI=";
+        };
+      })
+    ];
+
+    # We need some patches so it stops complaining about not being in a venv
+    postPatch = ''
+      substituteInPlace coq/consts.py \
+        --replace "VARS = TOP_LEVEL / \".vars\"" "VARS = Path.home() / \".cache/home/vars\"";
+      substituteInPlace coq/__main__.py \
+        --replace "_IN_VENV = _RT_PY == _EXEC_PATH" "_IN_VENV = True"
+    '';
+  };
+
+  coq-artifacts = pkgs.vimUtils.buildVimPlugin rec {
+    pname = "coq.artifacts";
+    version = "495429564e481cafeb044456da32c10cb631f948";
+
+    src = pkgs.fetchFromGitHub {
+      owner = "ms-jpq";
+      repo = "coq.artifacts";
+      rev = version;
+      sha256 = "sha256-AtkG2XRVZgvJzH2iLr7UT/U1+LXxenvNckdapnJV+8A=";
+    };
+  };
 }