Coq_checklib.Mod_checkingval set_indirect_accessor : (Opaqueproof.opaque -> Opaqueproof.opaque_proofterm) -> unitval check_module : Environ.env -> Names.Cset.t Names.Cmap.t -> Names.ModPath.t -> Declarations.module_body -> Names.Cset.t Names.Cmap.texception BadConstant of Names.Constant.t * Pp.t