Elimschemesval declare_prop_but_default_dependent_elim : Names.inductive -> unitDeclare an inductive should be eliminated dependently even though it's in Prop
val is_prop_but_default_dependent_elim : Names.inductive -> boolCheck if an inductive should be eliminated dependently even though it's in Prop
val pseudo_sort_quality_for_elim : Names.inductive -> Declarations.one_inductive_body -> Sorts.Quality.tLegacy API, returns the quality of the inductive except if it's prop_but_default_dependent_elim in which case we return Type instead.
val default_case_analysis_dependence : Environ.env -> Names.inductive -> boolReturns false on inductives which cannot be eliminated dependently or are in Prop without being declared prop_but_default_dependent_elim.
val elim_scheme : dep:bool -> to_kind:UnivGen.QualityOrSet.t -> Ind_tables.individual Ind_tables.scheme_kindInduction/recursion schemes
Case analysis schemes
val case_dep : Ind_tables.individual Ind_tables.scheme_kindval case_nodep : Ind_tables.individual Ind_tables.scheme_kindval casep_dep : Ind_tables.individual Ind_tables.scheme_kindval casep_nodep : Ind_tables.individual Ind_tables.scheme_kindRecursor names utilities
val lookup_eliminator : Environ.env -> Names.inductive -> UnivGen.QualityOrSet.t -> Names.GlobRef.tval elimination_suffix : UnivGen.QualityOrSet.t -> stringval make_elimination_ident : Names.Id.t -> UnivGen.QualityOrSet.t -> Names.Id.t