Skip to content

Commit 1670ae7

Browse files
Require Znumtheory before using it (#548)
For rocq-prover/stdlib#136
1 parent b41d5c1 commit 1670ae7

File tree

1 file changed

+1
-0
lines changed

1 file changed

+1
-0
lines changed

lib/IEEE754_extra.v

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -19,6 +19,7 @@
1919
floating-point numbers, on top of the Flocq library. *)
2020

2121
From Coq Require Import Reals SpecFloat ZArith Psatz Bool Eqdep_dec.
22+
From Coq Require Znumtheory.
2223
From Flocq Require Import Core Digits Operations Round Bracket Sterbenz
2324
BinarySingleNaN Binary Round_odd.
2425

0 commit comments

Comments
 (0)