Skip to content

Commit 0acf4f2

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

1 file changed

Lines changed: 1 addition & 0 deletions

File tree

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)