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_constant_alias : 
  Environ.env ->
  Names.Constant.t ->
  Declarations.constant_body ->
  unit

Check that a declaration whose user and canonical names differ is a valid alias of the canonical declaration already present in the environment.

val check_inductive_alias : 
  Environ.env ->
  Names.MutInd.t ->
  Declarations.mutual_inductive_body ->
  unit

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