fix to compile

math-comp · May 14, 2020 · cfaf5e7 · cfaf5e7
1 parent 7f431b8
commit cfaf5e7
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 1 deletion.
diff --git a/_CoqProject b/_CoqProject
@@ -16,6 +16,7 @@ theories/normedtype.v
 theories/forms.v
 theories/derive.v
 theories/summability.v
+theories/cauchyetoile.v
 theories/altreals/xfinmap.v
 theories/altreals/discrete.v
 theories/altreals/realseq.v

diff --git a/theories/cauchyetoile.v b/theories/cauchyetoile.v
@@ -3,7 +3,7 @@ From mathcomp Require Import ssreflect ssrfun ssrbool.
 From mathcomp Require Import ssrnat eqtype choice fintype bigop order ssralg ssrnum.
 From mathcomp Require Import complex.
 From mathcomp Require Import boolp reals ereal derive.
-Require Import classical_sets posnum topology normedtype landau integral.
+Require Import classical_sets posnum topology normedtype landau.
 
 (* Pour distinguer fonctions mesurables et integrables, utiliser des structures comme posrel. *)
 Import Order.TTheory GRing.Theory Num.Theory ComplexField Num.Def.