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