Problems with precedence

[wombaum...@gmail.com]

I am trying to  create a parser for the Coq Proof Assistant. The Grammar can be found here:

https://coq.inria.fr/distrib/current/refman/language/gallina-specification-language.html#recursive-functions

I also provide the grammar i so far implemented without the unneccessary parts here:

term : above_term | below_term;

above_term :
    <assoc=right> 'forall' binders ',' forall_term
    | <assoc=right> above_term '->' above_term
    | <assoc=right> above_term '->' below_term
    | <assoc=right> below_term '->' above_term
    | <assoc=right> below_term '->' below_term
    ;

below_term :
     <assoc = right> below_term arg (arg)*
    | qualid
    | sort
    | NUM
    | '_'
    | '(' term ')'
    ;

forall_term : term;


arg : <assoc=right>term| '(' IDENT ':=' term ')';
binders : binder (binder)*;
binder : name |<assoc=right>name (name)* ':' term | '(' name (name)* ':' term ')' |<assoc=right> name (':' term)? ':=' term;
name : IDENT | '_';

Full file can be downloaded on this site and is attached to the discussion: Coq Grammar File

Lets consider the following expression: a b -> b c -> forall n:nat, b

The parse tree i would expect to see (and is correct in terms of the language) is the following:

Please note that this pase tree can only be achieved by enforcing it with bracing (a b) -> (b c) -> forall n:nat, b. I want to have this tree without the braces.

However, this is the parse tree actually deriving from the above expression:

I don't understand, why the paser chooses a (below_expression -> above_expression) rule followed by the (arg) rule over the (above_expression -> above_expression) rule which i would like to see.

Any hints on how i can change my grammar would be much apreciated. Thx!