From 32315ab17d62eec68dec65c90fec2ec87d9d653e Mon Sep 17 00:00:00 2001
From: Yiyun Liu <liuyiyun@seas.upenn.edu>
Date: Wed, 17 Apr 2024 15:02:56 -0400
Subject: [PATCH] Remove deprecated and unused stdlib dependency

---
 Metalib/MetatheoryAtom.v | 1 -
 1 file changed, 1 deletion(-)

diff --git a/Metalib/MetatheoryAtom.v b/Metalib/MetatheoryAtom.v
index 15b86d0..c0e89a5 100644
--- a/Metalib/MetatheoryAtom.v
+++ b/Metalib/MetatheoryAtom.v
@@ -7,7 +7,6 @@
      Arthur Charg\'eraud *)
 
 Require Import Coq.Arith.Arith.
-Require Import Coq.Arith.Max.
 Require Import Coq.Classes.EquivDec.
 Require Import Coq.Lists.List.
 Require Import Coq.Structures.Equalities.