Command

[Rocq] A top-level directive in Rocq that controls the environment (like Definition, Theorem, Print, Check) rather than operating within a proof.