Coq_checklib.Mod_checkingval 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.tval constants_of_opaques : Environ.env -> opaques -> Names.Constant.t listval empty_opaques : opaques