diff --git a/theories/realalg.v b/theories/realalg.v
index 27cd847..7b930de 100644
--- 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.
 
 (*************************************************************************)