Up – Package index » rocq-runtime » Library rocq-runtime.kernel » Subtyping

Module `Subtyping`Source

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

Source

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