trying ot fix import statement

math-comp · Oct 4, 2024 · 6d98837 · 6d98837
1 parent 68b3afb
commit 6d98837
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/theories/function_spaces.v b/theories/function_spaces.v
@@ -3,7 +3,8 @@ From HB Require Import structures.
 From mathcomp Require Import all_ssreflect all_algebra finmap generic_quotient.
 From mathcomp Require Import boolp classical_sets functions.
 From mathcomp Require Import cardinality mathcomp_extra fsbigop.
-Require Import reals signed topology separation_axioms.
+
+From mathcomp Require Import reals signed topology separation_axioms.
 
 (**md**************************************************************************)
 (* # The topology of functions spaces                                         *)