Module Declare.Internal
val map_entry_body : f:('a Entries.proof_output -> 'b Entries.proof_output) -> 'a proof_entry -> 'b proof_entryval map_entry_type : f:(Constr.t option -> Constr.t option) -> 'a proof_entry -> 'a proof_entryval set_opacity : opaque:bool -> 'a proof_entry -> 'a proof_entryval get_fix_exn : 'a proof_entry -> Future.fix_exnval shrink_entry : EConstr.named_context -> 'a proof_entry -> 'a proof_entry * Constr.constr list