Internal (rocq-runtime.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