removing stray line

math-comp · Sep 19, 2024 · da31d3e · da31d3e
1 parent 0e7f4da
commit da31d3e
Showing 1 changed file with 0 additions and 1 deletion.
diff --git a/theories/topology.v b/theories/topology.v
@@ -4079,7 +4079,6 @@ HB.structure Definition OrderNbhs d :=
 HB.structure Definition OrderTopological d := 
   { T of Topological T & Order.Total d T & Order_isNbhs d T } .
 
-From mathcomp Require Import set_interval.
 Section order_topologies.
 
 Local Open Scope order_scope.