Skip to content

Commit 0acf4f2

Browse files
Require Znumtheory before using it
For rocq-prover/stdlib#136
1 parent 2d97cc4 commit 0acf4f2

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
@@ -23,6 +23,7 @@ Require Import SpecFloat.
2323
From Flocq Require Import Core Digits Operations Round Bracket Sterbenz
2424
BinarySingleNaN Binary Round_odd.
2525
Require Import ZArith.
26+
Require Znumtheory.
2627
Require Import Psatz.
2728
Require Import Bool.
2829
Require Import Eqdep_dec.

0 commit comments

Comments
 (0)