fix

math-comp · Oct 6, 2024 · 7c0a3f8 · 7c0a3f8
1 parent 804714f
commit 7c0a3f8
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/theories/separation_axioms.v b/theories/separation_axioms.v
@@ -4,7 +4,8 @@ From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
 From mathcomp Require Import archimedean.
 From mathcomp Require Import boolp classical_sets functions wochoice.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop set_interval.
-Require Import filter reals signed.
+From mathcomp Require Import filter.
+Require Import reals signed.
 Require Export topology.
 
 (**md**************************************************************************)