Clean up

math-comp · Jul 8, 2024 · a2d6098 · a2d6098
1 parent f0ef086
commit a2d6098
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/theories/realalg.v b/theories/realalg.v
@@ -1,8 +1,7 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
 From HB Require Import structures.
-From mathcomp Require Import all_ssreflect all_algebra all_field.
-From mathcomp Require Import archimedean bigenough.
+From mathcomp Require Import all_ssreflect all_algebra all_field bigenough.
 From mathcomp Require Import polyorder cauchyreals.
 
 (*************************************************************************)