diff --git a/FiniteSets/disjunction.v b/FiniteSets/disjunction.v
index 5775d8f..55a02a3 100644
--- a/FiniteSets/disjunction.v
+++ b/FiniteSets/disjunction.v
@@ -66,4 +66,6 @@ Section lor_props.
     - simple refine (Trunc_ind _ _).
       intros [x | x] ; apply x.
     - apply (fun x => tr (inl x)).
-  Defined.
\ No newline at end of file
+  Defined.
+
+End lor_props.