Module Recdef_plugin.Functional_principles_types
val compute_new_princ_type_from_rel : Constr.constr array -> Sorts.t array -> Constr.t -> Constr.types
Recdef_plugin.Functional_principles_types
val compute_new_princ_type_from_rel : Constr.constr array -> Sorts.t array -> Constr.t -> Constr.types