upd wrt master, minor simplications

math-comp · Jan 5, 2023 · 45751c8 · 45751c8
1 parent ea47d7f
commit 45751c8
Show file tree

Hide file tree

Showing 2 changed files with 213 additions and 320 deletions.
diff --git a/_CoqProject b/_CoqProject
@@ -38,6 +38,7 @@ theories/numfun.v
 theories/lebesgue_integral.v
 theories/summability.v
 theories/signed.v
+theories/smeasure.v
 theories/altreals/xfinmap.v
 theories/altreals/discrete.v
 theories/altreals/realseq.v