Module InferCumulativity
- val infer_inductive : Environ.env -> Entries.mutual_inductive_entry -> Entries.mutual_inductive_entry
- val dummy_variance : Entries.universes_entry -> Univ.Variance.t array
InferCumulativityval infer_inductive : Environ.env -> Entries.mutual_inductive_entry -> Entries.mutual_inductive_entryval dummy_variance : Entries.universes_entry -> Univ.Variance.t array