Skip to content

Commit 4fdf7ef

Browse files
andres-erbsenproux01
authored andcommitted
Import ZArith to use it in Rstruct.v
1 parent 4fced68 commit 4fdf7ef

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

reals_stdlib/Rstruct.v

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -25,7 +25,7 @@ liability. See the COPYING file for more details.
2525
(* # Compatibility with the real numbers of Coq *)
2626
(******************************************************************************)
2727

28-
From Coq Require Import Rdefinitions Raxioms RIneq Rbasic_fun Zwf.
28+
From Coq Require Import ZArith Rdefinitions Raxioms RIneq Rbasic_fun Zwf.
2929
From Coq Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def.
3030
From Coq Require Import Rtrigo1 Reals.
3131
From mathcomp Require Import all_ssreflect ssralg poly mxpoly ssrnum.

0 commit comments

Comments
 (0)