Import

[Rocq] A command in Rocq:(/programming-language-theory/concepts/rocq) that brings names from a loaded module into the current namespace, allowing unqualified access (often combined as Require Import).