Funind_plugin.Functional_principles_types
val compute_new_princ_type_from_rel : Environ.env -> Constr.constr array -> Sorts.t array -> Constr.t -> Constr.types