Module Declare.Internal

module Constant : sig ... end
val objVariable : Names.Id.t Libobject.Dyn.tag
val export_side_effects : Evd.side_effects -> unit

export_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