Syntax error with @

[fblanqui]

Description of the problem

Axiom T : Prop.
Axiom eq : forall {A}, A -> A -> Prop.
Axiom REFL : forall {a} (t : a), eq t t.
Axiom MK_COMB : forall {a b} {s t : a -> b} {u v : a}, eq s t -> eq u v -> eq (s u) (t v).
Definition type0 := Prop -> Prop.
Definition type1 := Prop -> Prop -> Prop.
Definition term1 (x0 : Prop) := @eq Prop x0.
Definition term2 := @eq Prop T.
Definition thm_4 (t : Prop) (h1 : @eq Prop t T) : @eq Prop t T := h1.
Definition thm_6 : @eq type1 (@eq Prop) (@eq Prop) := REFL (@eq Prop).
Definition thm_7a (t : Prop) (h1 : @eq Prop t T) : @eq type0 (term1 t) term2 := MK_COMB thm_6 (@thm_4 t h1).
Definition thm_7b (t : Prop) (h1 : @eq Prop t T) : @eq type0 (term1 t) term2 := MK_COMB (@thm_6) (@thm_4 t h1).
Definition thm_7c (t : Prop) (h1 : @eq Prop t T) : @eq type0 (term1 t) term2 := MK_COMB @thm_6 (@thm_4 t h1).
(*Error: Syntax error: '.' expected after [gallina] (in [vernac_aux]).*)

Coq Version

8.16.1

[SkySkimmer]

I guess that's just how the parsing levels turn out? I don't know if we can change it, especially if there are any users of @ as an infix.