package rocq-runtime
Module SubtypingSource
Source
val check_subtypes :
('a, UGraph.univ_inconsistency) Conversion.universe_state ->
Environ.env ->
Declarations.module_type_body ->
Declarations.module_type_body ->
'a