The rules for module instantiation specify that declarative element segments are dropped during instantiation [1]: ``` runelem𝑖({type et, init ref 𝑛, mode declarative}) = (elem.drop 𝑖) ``` But the prose only has a rule for active element segments: ``` For each element segment elem𝑖 in module.elems whose mode is of the form active {table tableidx 𝑖, offset einstr * 𝑖 end}, do: ... ``` I think we need an extension to the prose to mention that declarative segments are dropped during instantiation. [1] https://webassembly.github.io/spec/core/exec/modules.html#instantiation