From 5479f3abccffaceb9a35371e65a3d9937efb6c21 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 24 Sep 2025 18:32:02 +0900 Subject: [PATCH] fixes #1627 --- theories/normedtype_theory/num_normedtype.v | 1 - 1 file changed, 1 deletion(-) diff --git a/theories/normedtype_theory/num_normedtype.v b/theories/normedtype_theory/num_normedtype.v index 91a7b37b92..d2f291e814 100644 --- a/theories/normedtype_theory/num_normedtype.v +++ b/theories/normedtype_theory/num_normedtype.v @@ -1,5 +1,4 @@ (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) -From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix. From mathcomp Require Import rat interval zmodp vector fieldext falgebra. From mathcomp Require Import archimedean.