This file registers the ring corresponding to the MathComp-Analysis type realType to the tactic nsatz of Coq. This enables some automation used for example in the file trigo.v.
Reference: