diff --git a/lifetime/model/definitions.v b/lifetime/model/definitions.v
index 35fdc4a09faae5df40bac0cca1551ecc6962643f..6f00d3d21635ed0968df09797e6a07edd5520ac5 100644
--- a/lifetime/model/definitions.v
+++ b/lifetime/model/definitions.v
@@ -356,4 +356,5 @@ Proof. apply _. Qed.
 Global Definition atomic_lft_inhabited : Inhabited atomic_lft := _.
 Global Definition atomic_lft_eq_dec : EqDecision atomic_lft := _.
 Global Definition atomic_lft_countable : Countable atomic_lft := _.
+
 End basic_properties.