Proof General under spacemacs

extensions.el

(defvar coq-pre-extensions
  '(
    proof-general
    ))

(defun coq/init-proof-general ()
  "Initialize Proof General"
  (use-package proof-site
    :defer t
    :mode ("\\.v\\'" . coq-mode)
    :load-path
    "~/.nix-profile/share/emacs/site-lisp/ProofGeneral/generic"))

packages.el

(defvar coq-packages
  '(
    company-coq
    ))

(defun coq/init-company-coq ()
  (use-package company-coq
    :defer t
    :config
    (add-hook 'coq-mode-hook #'company-coq-initialize)))

I can't figure out how this works. I cloned as above and modified it to point to the correct proof general location, but opening Test.v treats it as a Verilog file. Can you help?