Remove unused Require Even (Even has been removed from stdlib in 8.19)

SkySkimmer · Jan 18, 2024 · cbd4b05 · cbd4b05
1 parent 9b70a13
commit cbd4b05
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/translations/param_cheap_packed.v b/translations/param_cheap_packed.v
@@ -241,7 +241,7 @@ Definition to := Type.
 MetaCoq Run (Translate emptyTC "nat" >>= tmDebug).
 
 Require Vector.
-Require Even.
+
 Unset Universe Checking.
 MetaCoq Run (Translate emptyTC "list" >>= tmDebug).
 Check (listᵗ : forall (A : TYPE), list A.1 -> Type).