two files named path.v #1412
Description
We should have noticed that earlier but there are now
two path.v files (in homotopy_theory and in ssreflect)
that cause a conflict when doing From mathcomp Require Import.
We may want to rename the one in MathComp-Analysis...