compatibility with coq 8.4

The most recent commit, to functors_transformations.v, is simple but needed to preserve compatibility
with coq 8.4.