From 57bafd3068d7bfa23e7fab0724dac452bd47ac36 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 6 Mar 2026 11:33:38 +0900
Subject: [PATCH 1/2] fixes #1885

---
 CHANGELOG_UNRELEASED.md    | 3 +++
 classical/classical_sets.v | 1 +
 2 files changed, 4 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 5b7f660af..df91d2c0a 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -256,6 +256,9 @@
 - in `lebesgue_integral_nonneg.v`:
   + lemma `integral_setU_EFin`
 
+- in `classical_sets.v`:
+  + lemma `mem_setT`
+
 ### Removed
 
 - in `weak_topology.v`:
diff --git a/classical/classical_sets.v b/classical/classical_sets.v
index 8f6660605..c35170c97 100644
--- a/classical/classical_sets.v
+++ b/classical/classical_sets.v
@@ -507,6 +507,7 @@ Implicit Types A B C D : set T.
 
 Lemma mem_set {A} {u : T} : A u -> u \in A. Proof. by rewrite inE. Qed.
 Lemma set_mem {A} {u : T} : u \in A -> A u. Proof. by rewrite inE. Qed.
+#[deprecated(since="mathcomp-analysis 1.16.0", use=in_setT)]
 Lemma mem_setT (u : T)    : u \in [set: T]. Proof. by rewrite inE. Qed.
 Lemma mem_setK {A} {u : T} : cancel (@mem_set A u) set_mem. Proof. by []. Qed.
 Lemma set_memK {A} {u : T} : cancel (@set_mem A u) mem_set. Proof. by []. Qed.

From 07d83f2c608f85307d6679ae7955ae8728cc95c9 Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Fri, 6 Mar 2026 11:35:26 +0900
Subject: [PATCH 2/2] fixes #1880

---
 theories/derive.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/derive.v b/theories/derive.v
index b0862eb08..836a54614 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -76,7 +76,7 @@ Definition diff (F : filter_on V) (_ : phantom (set (set V)) F) (f : V -> W) :=
 Local Notation "''d' f x" := (@diff _ (Phantom _ (nbhs x)) f).
 
 Fact diff_key : forall T, T -> unit. Proof. by constructor. Qed.
-CoInductive differentiable_def (f : V -> W) (x : filter_on V)
+Variant differentiable_def (f : V -> W) (x : filter_on V)
   (phF : phantom (set (set V)) x) : Prop := DifferentiableDef of
   (continuous ('d f x) /\
   f = cst (f (lim x)) + 'd f x \o center (lim x) +o_x (center (lim x))).