From 0acf4f2326c008128372ae1a25e7d808f8e24f32 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 4 May 2025 14:40:28 -0400 Subject: [PATCH] Require Znumtheory before using it For https://github.com/rocq-prover/stdlib/pull/136 --- lib/IEEE754_extra.v | 1 + 1 file changed, 1 insertion(+) diff --git a/lib/IEEE754_extra.v b/lib/IEEE754_extra.v index f7c2487b93..803702db7b 100644 --- a/lib/IEEE754_extra.v +++ b/lib/IEEE754_extra.v @@ -23,6 +23,7 @@ Require Import SpecFloat. From Flocq Require Import Core Digits Operations Round Bracket Sterbenz BinarySingleNaN Binary Round_odd. Require Import ZArith. +Require Znumtheory. Require Import Psatz. Require Import Bool. Require Import Eqdep_dec.