What does the at sign @ mean in Coq - especially in the context of Gallina terms?

I was trying to understand what the @ at sign did in Coq in all contexts. The context that I saw this was that I was experimenting with printing and removing notations (or as much as I could) in Coq. In particular, I was printing (Gallina) terms with the Set Printing All. I defined my own addition and nats and got this when I did that

my_add_eq = 
fun x y : my_nat => @eq_refl my_nat (my_add x y)
     : forall x y : my_nat, @eq my_nat (my_add x y) (my_add x y)

but I wasn't sure what the @ sign meant. What does it mean?

---

Note I saw this question Refine and @ (at) symbol in Coq 8.5pl1 but it seems that they are using @ in the context of a proof where I am seeing it in a different context (I am printing a Gallina term). To be honest I don't fully appreciate the answer to that question. Perhaps it is related to my question but I cannot tell. Perhaps from reading that more carefully I might need implicit arguments to really appreciate what @ mean? To my surprise googling What does the at sign @ in coq do didn't yield to much except that SO question I posted. A reference to the coq manual/documentation wouod be ideal (I did try to search in the docs at sign and @ but it didn't yield anything useful).

---

Perhaps I can share my script:

    Inductive my_nat : Type :=
    | O : my_nat
    | S : my_nat->my_nat.

    Fixpoint my_add (n1:my_nat) (n2:my_nat) :=
        match n1 with
            | O => n2
            | S n1' => S (my_add (n1') (n2))
        end.

    Notation "x [+] y" := (my_add x y)
                       (at level 50, left associativity)
                       : nat_scope.

    Lemma my_add_eq:
      forall (x y : my_nat),
        x [+] y = x [+] y.
    Proof.
      auto.
    Qed.
    
    Print my_add_eq.
    Set Printing All.
    Print my_add_eq.

from Recent Questions - Stack Overflow https://ift.tt/3zQLeC1
https://ift.tt/eA8V8J