coq - Coq に括弧を出力させることはできますか?

Question

私はCoqを初めて使用し、集合論的証明の作成に取り組んでいます。

括弧が省略されていて、式が読みにくいことに気付きました。例えば、

1 subgoal
A, B : {set T}
H : B \subset A
______________________________________(1/1)
A :\: A :|: A :&: B = B

しかし、Coqに印刷してもらいたい(A :\: A) :|: (A :&: B) = Bです。上記の出力は、次のコードによって得られます。

Require Import ssreflect ssrbool ssrnat fintype finset.
Theorem a_a_b__b' (A B : {set T}) : B \subset A -> (A :\: (A :\: B)) = B.
Proof.
  move=> H.
  rewrite setDDr.

setDDr驚いたことに、finset.vの元のコーディングを見ると、次のように括弧が付いています。

Lemma setDDr A B C : A :\: (B :\: C) = (A :\: B) :|: (A :&: C).
Proof. by rewrite !setDE setCI setIUr setCK. Qed.

だから私はなぜ括弧が消えるのか、どのように Coq に CoqIde で括弧を明示的に出力させるのか疑問に思っています。