ElimschemesInduction/recursion schemes
val elim_scheme : dep:bool -> to_kind:UnivGen.QualityOrSet.t -> Ind_tables.individual Ind_tables.scheme_kindCase 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