where is Coq aac_tactics installed?

Question

I was testing the AAC tactics library for rewrites modulo associativity and commutativity. According to a Coq website, one should:

Depending on your installation, either modify the following two lines, or add them to your .coqrc files, replacing "." with the path to the aac_tactics library.

Add Rec LoadPath "." as AAC_tactics.
Add ML Path ".".
Require Import AAC.
Require Instances.

But I don't know how to find the path to the aac_tactics library, and using "." didn't work.

I installed Coq under Ubuntu 16.04 LTS along the lines of:

opam repo add coq-released https://coq.inria.fr/opam/released
opam install coq-mathcomp-ssreflect.1.6
opam install coq-aac-tactics.8.5.1

Does anyone know where to find the library location?

Answer 1

It seems this will work (at least for this tutorial):

(*
Add Rec LoadPath "." as AAC_tactics.
Add ML Path ".".
*)
Require Import AAC_tactics.AAC.
Require Import AAC_tactics.Instances.

Usually, OPAM stores its stuff in ~/.opam. You can look it up with the following command in your terminal:

$ opam config var root

Then you can have multiple configurations called switches (it's mainly for keeping different version of the OCaml compiler). The root for your current switch can be found this way:

$ opam config var prefix

And the libraries for the current switch are kept in the directory which you can look up here:

$ opam config var lib

There you'll find the AAC_tactics subdirectory, which is the prefix we needed to add to our imports above.