package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

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

package rocq-runtime

Module SubtypingSource

Module `Subtyping`Source