Notation in the Reals Library

Using Coq
1

I am currently reading through the Reals documentation.
In the file Raxioms, the third axiom given is :
https://coq.inria.fr/library/Coq.Reals.Raxioms.html#
Axiom Rplus_opp_r : forall r:R, r + - r = 0.
Hint Resolve Rplus_opp_r: real.
I would like to understand how the notation 0 has been introduced, as I can’t find it in explicitely anywhere. Do you have any clue ?

Thanks !
-wazdra

2

I might be wrong, but a quick search suggests that it’s defined in r_syntax.ml. It’s basically IZR Z0.

3

Ok, thank you ! I haven’t encountered CaML files in Coq and don’t know how it works yet… I guess I’ll get back to that later.