https://github.com/math-comp/analysis/blob/1ab682517f25e7f661e3b6dee2453778a535260f/theories/measure.v#L3575 the measure `P` should not be implicit
analysis/theories/measure.v
Line 3575 in 1ab6825
the measure
Pshould not be implicit