Import ZArith to use it in Rstruct.v

math-comp · Jan 8, 2025 · 4fdf7ef · 4fdf7ef
1 parent 4fced68
commit 4fdf7ef
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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.