Library Coq.Reals.Rregisternames


Require Import Reals.

Register names in the Reals library used by plugins