From a2d6098c921a301236932f3683a63cfec0c9cfc7 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Mon, 8 Jul 2024 13:27:53 +0200 Subject: [PATCH] Clean up --- theories/realalg.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) 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. (*************************************************************************)