fixes #1627 (#1725)

affeldt-aist · web-flow · commit c55da8cb9699 · 2025-09-24T21:29:59.000+09:00
diff --git 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.

Original file line number	Diff line number	Diff line change
`@@ -1,5 +1,4 @@`
`1`	`1`	`(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *)`
`2`		`-From HB Require Import structures.`
`3`	`2`	`From mathcomp Require Import all_ssreflect ssralg ssrint ssrnum finmap matrix.`
`4`	`3`	`From mathcomp Require Import rat interval zmodp vector fieldext falgebra.`
`5`	`4`	`From mathcomp Require Import archimedean.`