How to change Coq Version in Proof General?

Question

I have some code that only compiles coq code in Coq 8.09.0 . The version that I normally use is the most up-to-date version now which is Coq 8.11.0. I was able to create a new environment using opam switch and installed Coq 8.09.0 there. I successfully compiled all of the files with this version; however, I can't use proof general in emacs as it is still using Coq 8.11.0. I was wondering how I could make Proof General use a different opam instance using opam switch in Emacs. I have tried doing the following in the eshell

opam switch vst
eval $(opam env)

where vst is the name of the switch as seen in the output of opam switch in my terminal:

#   switch   compiler                                                                         description
    4.10.0   ocaml-base-compiler.4.10.0                                                       4.10.0
    default  base-bigarray.base,base-threads.base,base-unix.base,ocaml.4.02.3,ocaml-config.1  default
->  vst      ocaml-base-compiler.4.09.0                                                       vst

However, the output of the eval $(opam env) line is the following:

Symbol’s function definition is void: opam

Which doesn't make sense since it understands what opam means as it was able to do the first command fine. Is there a proper way of doing opam switch to change what emacs uses? Is there a way to explicitly tell Proof General which instance of Coq it should use? Should I just uninstall Coq 8.11.0 and install Coq 8.09.0 directly using pacman (I am using manjaro)?

Answer 1

Using M-x and searching for "opam version" gave me the promising option

tuareg-opam-update-env

which allows one to switch environments. Doing this to switch to vst before opening a coq file and not autochecking the version of Coq seemed to work fine. Of course, this assumes one has tuareg already installed.