In theories/normedtype.v ```Coq (* Ideally, R should be an instance of realType here, rather than a section variable. *) ``` C.f. https://github.com/math-comp/analysis/pull/1347