Skip to content

Coq/Rocq support still uses hard-coded coq/user-contrib #13532

@rlepigre-skylabs-ai

Description

@rlepigre-skylabs-ai

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

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions