typo

math-comp · Oct 30, 2024 · 1c5523e · 1c5523e
1 parent ac6a5e6
commit 1c5523e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/lebesgue_integral.v b/theories/lebesgue_integral.v
@@ -87,7 +87,7 @@ From mathcomp Require Import lebesgue_measure numfun realfun function_spaces.
 (* Coq functions.                                                             *)
 (* Also, assume that f (e.g., cst, indic) is equipped with the structure of   *)
 (* MeasurableFun. For f to be equipped with the structure of SimpleFun        *)
-(* (resp. NonNegSimpleFun), one need locallu to import HBSimple (resp.        *)
+(* (resp. NonNegSimpleFun), one need locally to import HBSimple (resp.        *)
 (* HBNNSimple) and to instantiate FiniteImage (resp. NonNegFun) locally.      *)
 (*                                                                            *)
 (******************************************************************************)