Proof General is a frontend for Coq but it comes with some custom variables you can set up. You can customize the program name, the program arguments and so on by setting the variables provided by Proof General so that if you have custom Coq binaries you may still use them.

This means we can can have opam manage our Coq environment to have different versions and theories for different projects.

It’s as easy as installing the opam package from MELPA and then adding the following to your init.el.

(use-package opam
  :ensure t
  :config
  (opam-init))

(use-package proof-general
  :ensure t
  :after (opam) ;; as I am using opam to manage my coq environment loads after that
  :mode ("\\.v'" . coq-mode)
  :custom
    (coq-use-project-file t))

Unfortunately this relies on the currently selected ``opam switch’’ and therefore you will need to switch to the corrent opam installation before starting EMACS to interact with Coq.