Coq_checklib.Mod_checkingtype opaques = Names.Cset.t Names.Cmap.tval set_indirect_accessor : (Opaqueproof.opaque -> Opaqueproof.opaque_proofterm) -> unitval check_module : Environ.env -> opaques -> Retroknowledge.action list -> Names.ModPath.t -> Mod_declarations.module_body -> opaquesexception BadConstant of Names.Constant.t * Pp.t