From 4fdf7ef6936a9383e3a27e0957bf97dbc5e65a38 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 7 Jan 2025 01:05:36 +0000 Subject: [PATCH] Import ZArith to use it in Rstruct.v --- reals_stdlib/Rstruct.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/reals_stdlib/Rstruct.v b/reals_stdlib/Rstruct.v index 998ed7690..760cd14e5 100644 --- a/reals_stdlib/Rstruct.v +++ b/reals_stdlib/Rstruct.v @@ -25,7 +25,7 @@ liability. See the COPYING file for more details. (* # Compatibility with the real numbers of Coq *) (******************************************************************************) -From Coq Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf. +From Coq Require Import ZArith Rdefinitions Raxioms RIneq Rbasic_fun Zwf. From Coq Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def. From Coq Require Import Rtrigo1 Reals. From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum.