package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

Module `Inductive.Template`Source

Sourceval bind_kind : Sorts.t -> int option * int option

Sourceval template_subst_sort : template_subst -> Sorts.t -> Sorts.t

val max_template_quality : 
  Sorts.Quality.t ->
  Sorts.Quality.t ->
  Sorts.Quality.t

Qualities must be above_prop