From a1e940cc4d4e6581aa8115db41ed7b0e7eb5f733 Mon Sep 17 00:00:00 2001
From: Niels <nnmvdw@gmail.com>
Date: Fri, 4 Aug 2017 20:55:47 +0200
Subject: [PATCH] Added proof of HSet

---
 int/Integers.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/int/Integers.v b/int/Integers.v
index e06192f..1a8b11e 100644
--- a/int/Integers.v
+++ b/int/Integers.v
@@ -659,7 +659,7 @@ Section Isomorphic.
   Instance Z'_set : IsHSet Z'.
   Proof.
     apply (trunc_equiv Int Int_to_Z').
-  Defined
+  Defined.
 
   Definition Z_to_Z' : Z -> Z'.
   Proof.