Note that this is just a consequence of symbols not being imported from
realizations. If Coq files were generated with "Require Import" directives
rather than just "Require", the change would have been completely
transparent. This is not reason enough to switch to "Require Import" but
it should be kept in mind.