return {
  "whonore/Coqtail",
  ft = "coq",
  init = function()
    vim.g.coqtail_nomap = 1
    vim.g.coqtail_noimap = 1
  end,
  keys = {
    { "<localleader>j", "<cmd>CoqNext<cr>", desc = "Step Forward" },
    { "<localleader>k", "<cmd>CoqUndo<cr>", desc = "Step Backwards" },
    { "C-<Down>", "<cmd>CoqNext<cr>", desc = "Step Forward", mode = "i" },
    { "C-<Up>", "<cmd>CoqUndo<cr>", desc = "Step Backwards", mode = "i" },
    { "<localleader>l", "<cmd>CoqToLine<cr>", desc = "Step Here" },
    { "<localleader>h", "<Plug>CoqCheck", desc = "Check term", mode = "v" },
    { "<localleader>h", "<Plug>CoqCheck", desc = "Check term", mode = "n" },
    { "<localleader>a", "<Plug>CoqAbout", desc = "Show Information", mode = "v" },
    { "<localleader>a", "<Plug>CoqAbout", desc = "Show Information", mode = "n" },
    { "<localleader>p", "<Plug>CoqPrint", desc = "Print Definition", mode = "v" },
    { "<localleader>p", "<Plug>CoqPrint", desc = "Print Definition", mode = "n" },
    { "<localleader>f", "<Plug>CoqLocate", desc = "Locate Definition", mode = "v" },
    { "<localleader>f", "<Plug>CoqLocate", desc = "Locate Definition", mode = "n" },
    { "<localleader>s", "<Plug>CoqSearch", desc = "Show Theorems", mode = "v" },
    { "<localleader>s", "<Plug>CoqSearch", desc = "Show Theorems", mode = "n" },
  },
}