Subtyping (rocq-runtime.Subtyping)

val check_subtypes : ('a, Conversion.graph_inconsistency) Conversion.universe_state -> Environ.env -> Names.ModPath.t -> Names.ModPath.t -> Mod_declarations.module_type_body -> 'a

val check_polymorphic_universes : Environ.env -> UVars.AbstractContext.t -> UVars.AbstractContext.t -> bool