From 8275649ebd9d738e362d9f9dae2992a7d8e038cf Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Thu, 11 May 2023 23:16:43 +0900
Subject: [PATCH] minor fix

---
 theories/kernel.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/theories/kernel.v b/theories/kernel.v
index 76c1d3c46..c2c6efa49 100644
--- a/theories/kernel.v
+++ b/theories/kernel.v
@@ -166,7 +166,8 @@ HB.mixin Record Kernel_isSFinite_subdef d d'
 
 HB.structure Definition SFiniteKernel d d'
     (X : measurableType d) (Y : measurableType d') (R : realType) :=
-  { k of @Kernel _ _ _ _ R k & Kernel_isSFinite_subdef _ _ X Y R k }.
+  { k of @Kernel _ _ _ _ R k &
+         Kernel_isSFinite_subdef _ _ X Y R k }.
 Notation "R .-sfker X ~> Y" := (SFiniteKernel.type X Y R).
 Arguments sfinite_kernel_subdef {_ _ _ _ _} _.