unnecessary parens

affeldt-aist · Mar 10, 2024 · 48ff7f0 · 48ff7f0
1 parent 8069cbf
commit 48ff7f0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/lib/ssrR.v b/lib/ssrR.v
@@ -906,7 +906,7 @@ Section temporary_lemmas.
 Local Open Scope ring_scope.
 
 Lemma sumRE (I : Type) (r : seq I) (P : pred I) (F : I -> R) :
-  (\sum_(i <- r | P i) F i)%coqR = (\sum_(i <- r | P i) F i).
+  (\sum_(i <- r | P i) F i)%coqR = \sum_(i <- r | P i) F i.
 Proof. by []. Qed.
 
 Lemma bigmaxRE (I : Type) (r : seq I) (P : pred I) (F : I -> R) :