From 587514efff82aac56bc7a5ca0db39fdd1c81871d Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 3 Nov 2024 16:39:01 +0000 Subject: [PATCH] Require Import ZArith before using it in ModularArithmeticTheorems.v --- src/Arithmetic/ModularArithmeticTheorems.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Arithmetic/ModularArithmeticTheorems.v b/src/Arithmetic/ModularArithmeticTheorems.v index 45f51ac983..8f15ed2201 100644 --- a/src/Arithmetic/ModularArithmeticTheorems.v +++ b/src/Arithmetic/ModularArithmeticTheorems.v @@ -1,4 +1,4 @@ -From Coq Require Import Lia Morphisms Morphisms_Prop. +From Coq Require Import ZArith Lia Morphisms Morphisms_Prop. Require Import Crypto.Spec.ModularArithmetic. Require Import Crypto.Arithmetic.ModularArithmeticPre.