Require Import BinNat before using it in ParseArithmetic.v

mit-plv · Nov 3, 2024 · 9bf41bc · 9bf41bc
1 parent ee1e322
commit 9bf41bc
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/Util/Strings/ParseArithmetic.v b/src/Util/Strings/ParseArithmetic.v
@@ -1,5 +1,5 @@
 From Coq Require Import Ascii String List.
-From Coq Require Import BinNums.
+From Coq Require Import BinNat.
 From Coq Require Import QArith.
 From Coq Require Import BinInt.
 Require Import Crypto.Util.Option.