From 9bf41bc65f9cfb7263eda84fcfc878fe8da45ff7 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Sun, 3 Nov 2024 16:40:51 +0000 Subject: [PATCH] Require Import BinNat before using it in ParseArithmetic.v --- src/Util/Strings/ParseArithmetic.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Util/Strings/ParseArithmetic.v b/src/Util/Strings/ParseArithmetic.v index ff8b1613a7..178a4c6813 100644 --- 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.