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