Hi. While I was writing a Coq formatter, I encountered a problem of not being able to get information of parentheses.

Consider the following `Theorem`

(from Induction: Proof by Induction in Software Foundation).

```
Theorem add_assoc : ∀ n m p : nat,
n + (m + p) = (n + m) + p.
```

The parentheses in `(n + m) + p`

are actually unnecessary as `+`

has left-associativity, but the ones in `n + (m + p)`

are necessary. The problem is that I couldn’t find a way to get the information of where parentheses are from an AST (`Vernacexpr.vernac_control`

). (Btw, in Haskell, I could get the information via `HsPar`

of `HsExpr`

).

I thought I’d infer the parentheses’ positions from an AST by comparing the level of the operator of the reversed side (LHS if the operator has right associativity, and vice versa) if I got an operator’s associativity (either left or right assoc.). However, I couldn’t find the way for this either.

Is it possible to get parentheses’ positions or an operator’s associativity, or is there another way to pretty-print the theorem with parentheses?

I’m using Coq 8.17.1.