diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 697e29672..feda99901 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -50,6 +50,9 @@
 
 ### Generalized
 
+- in `derive.v`:
+  + `derive_cst`, `derive1_cst`
+
 ### Deprecated
 
 ### Removed
diff --git a/theories/derive.v b/theories/derive.v
index febdfe08d..0fb8fa1ae 100644
--- a/theories/derive.v
+++ b/theories/derive.v
@@ -1241,7 +1241,7 @@ move=> dfx; apply: DeriveDef; first exact: derivableZ.
 by rewrite deriveZ // derive_val.
 Qed.
 
-Lemma derive_cst (k : R) (x v : V) : 'D_v (cst k) x = 0.
+Lemma derive_cst (k : W) (x v : V) : 'D_v (cst k) x = 0.
 Proof. by rewrite derive_val. Qed.
 
 End Derive_lemmasVW.
@@ -1389,7 +1389,8 @@ Lemma is_derive_shift {R : numFieldType} x v (k : R) :
   is_derive x v (shift k) v.
 Proof. by apply: DeriveDef => //; rewrite derive_val addr0. Qed.
 
-Lemma derive1_cst {R : numFieldType} (k : R) t : (cst k)^`() t = 0.
+Lemma derive1_cst {R : numFieldType} (V : normedModType R) (k : V) t :
+  (cst k)^`() t = 0.
 Proof. by rewrite derive1E derive_cst. Qed.
 
 Lemma derive1Mr {R : numFieldType} (f : R -> R) (x r : R) :