Require Import ZArith before using it in ModularArithmeticTheorems.v

mit-plv · Nov 3, 2024 · 587514e · 587514e
1 parent 7ccd89f
commit 587514e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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.