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 effectseff
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