From 2ebdcf29ae90a1eb6c5b2e7cc55fc382f41b1a24 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Thu, 5 Feb 2026 16:45:10 +0100 Subject: [PATCH] Fix #1837 Fix https://github.com/math-comp/analysis/pull/1836 --- theories/charge.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/charge.v b/theories/charge.v index 8c89636c7..a26756493 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -7,7 +7,7 @@ From mathcomp Require Import unstable. From mathcomp Require Import mathcomp_extra boolp classical_sets cardinality. From mathcomp Require Import functions fsbigop set_interval reals. From mathcomp Require Import interval_inference ereal topology numfun. -From mathcomp Require Import normedtype sequences esum measure realfun. +From mathcomp Require Import normedtype derive sequences esum measure realfun. From mathcomp Require Import lebesgue_measure lebesgue_integral. (**md**************************************************************************) @@ -84,7 +84,7 @@ Reserved Notation "{ 'additive_charge' 'set' T '->' '\bar' R }" Reserved Notation "{ 'charge' 'set' T '->' '\bar' R }" (at level 36, T, R at next level, format "{ 'charge' 'set' T '->' '\bar' R }"). -Reserved Notation "'d nu '/d mu" (at level 10, nu, mu at next level, +Reserved Notation "'d nu '/d mu" (mu at next level, format "''d' nu ''/d' mu"). Reserved Notation "nu .-negative_set" (at level 2, format "nu .-negative_set"). Reserved Notation "nu .-positive_set" (at level 2, format "nu .-positive_set").