From b06c59339b281fd03a98adfe9a2cc4839d39c8c3 Mon Sep 17 00:00:00 2001 From: Niels Date: Mon, 31 Jul 2017 14:54:20 +0200 Subject: [PATCH] Small fix --- FiniteSets/disjunction.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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.