Module Declare.Internal

val map_entry_body : f:('a Entries.proof_output -> 'b Entries.proof_output) -> 'a proof_entry -> 'b proof_entry
val map_entry_type : f:(Constr.t option -> Constr.t option) -> 'a proof_entry -> 'a proof_entry
val set_opacity : opaque:bool -> 'a proof_entry -> 'a proof_entry
val shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list
type constant_obj
val objConstant : constant_obj Libobject.Dyn.tag
val objVariable : unit Libobject.Dyn.tag