Declare.InternalSourceexport_side_effects eff makes the side effects eff global. This usually happens at the end of a proof (during Qed or Defined), but one may need to declare them by hand, for example because the tactic was run as part of a command