From 24eb01a1f0c6e7f9e8e02bf65328ad8f6fe5c0d2 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 26 May 2025 15:46:25 +0900 Subject: [PATCH 1/2] fixes #1632 --- CHANGELOG_UNRELEASED.md | 3 +++ theories/derive.v | 5 +++-- 2 files changed, 6 insertions(+), 2 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 697e29672a..eb5e853298 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -50,6 +50,9 @@ ### Generalized +- in `derive.v`: + + `derive_cstr`, `derive1_cst` + ### Deprecated ### Removed diff --git a/theories/derive.v b/theories/derive.v index febdfe08d8..0fb8fa1ae6 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) : From a314df3e992c7e4cb77adc1fe56846956d91ab6d Mon Sep 17 00:00:00 2001 From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com> Date: Mon, 26 May 2025 16:25:22 +0900 Subject: [PATCH 2/2] Update CHANGELOG_UNRELEASED.md --- CHANGELOG_UNRELEASED.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index eb5e853298..feda99901b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -51,7 +51,7 @@ ### Generalized - in `derive.v`: - + `derive_cstr`, `derive1_cst` + + `derive_cst`, `derive1_cst` ### Deprecated