Library Coq.Reals.Rregisternames
Require
Import
Reals
.
Register names in the Reals library used by plugins