From 6e04d502b9fb42fe89e96e336ac9265988a795a3 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Tue, 22 Apr 2025 11:49:22 +0900
Subject: [PATCH] typo

---
 CHANGELOG_UNRELEASED.md |  3 +++
 theories/kernel.v       | 18 +++++++++++++++---
 2 files changed, 18 insertions(+), 3 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 67bb43c3b6..3a2ed8859f 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -8,6 +8,9 @@
 
 ### Renamed
 
+- in `kernel.v`:
+  + `isFiniteTransition` -> `isFiniteTransitionKernel`
+
 ### Generalized
 
 ### Deprecated
diff --git a/theories/kernel.v b/theories/kernel.v
index 7d73d392d8..a9cce84569 100644
--- a/theories/kernel.v
+++ b/theories/kernel.v
@@ -267,16 +267,28 @@ HB.structure Definition SigmaFiniteTransitionKernel
 Notation "R .-sigmafker X ~> Y" := (sigma_finite_kernel X%type Y R).
 
 (* interface for finite transition kernel *)
-HB.mixin Record isFiniteTransition
+HB.mixin Record isFiniteTransitionKernel
     d d' (X : measurableType d) (Y : measurableType d')
     (R : realType) (k : X -> {measure set Y -> \bar R}) := {
   kernel_finite_transition : forall x, fin_num_fun (k x) }.
 
+#[deprecated(since="mathcomp-analysis 1.11.0",
+             note="Use isFiniteTransitionKernel instead.")]
+Notation isFiniteTransition x1 x2 x3 x4 x5 x6 :=
+  (isFiniteTransitionKernel x1 x2 x3 x4 x5 x6).
+
 #[short(type=finite_transition_kernel)]
 HB.structure Definition FiniteTransitionKernel
     d d' (X : measurableType d) (Y : measurableType d') (R : realType) :=
   { k of @SFiniteKernel _ _ _ _ _ k &
-         isFiniteTransition _ _ X Y R k }.
+         isFiniteTransitionKernel _ _ X Y R k }.
+
+Module isFiniteTransition.
+#[deprecated(since="mathcomp-analysis 1.11.0",
+             note="Use isFiniteTransitionKernel.Build instead.")]
+Notation Build x1 x2 x3 x4 x5 x6 :=
+  (isFiniteTransitionKernel.Build x1 x2 x3 x4 x5 x6) (only parsing).
+End isFiniteTransition.
 
 Notation "R .-ftker X ~> Y" := (finite_transition_kernel X%type Y R).
 
@@ -348,7 +360,7 @@ by rewrite (lt_trans (kr x)) ?ltry.
 Qed.
 
 HB.instance Definition _ :=
-  @isFiniteTransition.Build d d' X Y R k finite_transition_finite.
+  @isFiniteTransitionKernel.Build d d' X Y R k finite_transition_finite.
 
 HB.instance Definition _ :=
   @isMeasureFamUub.Build d d' X Y R k measure_uub.