https://github.com/math-comp/analysis/blob/129c71c59fb4769623f1043c6b65b292e700fa36/classical/functions.v#L392 should be `phant_mem_fun` instead of `phant_funS`