From 092644ffdf4d25bd5e37f75f3d82c89e924c7815 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 3 Apr 2026 13:59:46 +0200 Subject: [PATCH] Adapt to https://github.com/rocq-prover/rocq/pull/21851 --- analysis_stdlib/Rstruct_topology.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/analysis_stdlib/Rstruct_topology.v b/analysis_stdlib/Rstruct_topology.v index 22af9c9b5..df42aa254 100644 --- a/analysis_stdlib/Rstruct_topology.v +++ b/analysis_stdlib/Rstruct_topology.v @@ -4,9 +4,9 @@ (* Extension to Rstruct.v (lemmas about continuity) *) (******************************************************************************) -Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf. -Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def. -Require Import Rtrigo1 Reals. +From Stdlib Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf. +From Stdlib Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def. +From Stdlib Require Import Rtrigo1 Reals. From HB Require Import structures. From mathcomp Require Import all_ssreflect_compat ssralg ssrnum archimedean. From mathcomp Require Import boolp classical_sets reals interval_inference.