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.