This is really only used in installation rules for theories, where the target section is lib_root and the path is coq/user-contrib/.... See the discussion here.
It's not really clear to me what the right solution is. Should lib_root/coq/user-contrib be a new section? On the other hand, I'm hoping that this directory will stop existing in a not-so-distant future, and be replaced by a notion of Rocq package (see rocq-prover/rfcs#101, rocq-prover/rocq#21564).
CC @Alizter @SkySkimmer
This is really only used in installation rules for theories, where the target section is
lib_rootand the path iscoq/user-contrib/.... See the discussion here.It's not really clear to me what the right solution is. Should
lib_root/coq/user-contribbe a new section? On the other hand, I'm hoping that this directory will stop existing in a not-so-distant future, and be replaced by a notion of Rocq package (see rocq-prover/rfcs#101, rocq-prover/rocq#21564).CC @Alizter @SkySkimmer