package coq

You can search for identifiers within the package.

in-package search v0.2.0

Module `InferCumulativity`Source

val infer_inductive : 
  env_params:Environ.env ->
  (Univ.Level.t * Univ.Variance.t option) array ->
  Entries.one_inductive_entry list ->
  Univ.Variance.t array