Module Recdef_plugin.Functional_principles_types

val generate_functional_principle : Evd.evar_map Stdlib.ref -> bool -> Constr.types -> Sorts.t array option -> Names.Id.t option -> Constr.pconstant array -> int -> (EConstr.constr array -> int -> Tacmach.tactic) -> unit
exception No_graph_found
val make_scheme : Evd.evar_map Stdlib.ref -> (Constr.pconstant * Sorts.family) list -> Safe_typing.private_constants Entries.definition_entry list
val build_scheme : (Names.Id.t * Libnames.qualid * Sorts.family) list -> unit
val build_case_scheme : (Names.Id.t * Libnames.qualid * Sorts.family) -> unit