From 895050d155c7262a699efbceaa73764571227c02 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Thu, 4 Feb 2016 13:38:33 -0500
Subject: [PATCH] fix(*): fix broken files

---
 group_theory/basic.hlean         | 8 +-------
 group_theory/constructions.hlean | 2 +-
 homotopy/sample.hlean            | 4 ++--
 3 files changed, 4 insertions(+), 10 deletions(-)

diff --git a/group_theory/basic.hlean b/group_theory/basic.hlean
index 1d5389f..d5063fa 100644
--- a/group_theory/basic.hlean
+++ b/group_theory/basic.hlean
@@ -13,17 +13,11 @@ Basic group theory
   The only relevant defintions are the trivial group (in types/unit) and some files in algebra/
 -/
 
-<<<<<<< HEAD
-import algebra.group types.pointed types.pi
-
-open eq algebra pointed function is_trunc pi
-
-=======
 import types.pointed types.pi algebra.bundled algebra.category.category
 
 open eq algebra pointed function is_trunc pi category equiv is_equiv
 set_option class.force_new true
->>>>>>> origin/master
+
 namespace group
 
   definition pointed_Group [instance] (G : Group) : pointed G := pointed.mk one
diff --git a/group_theory/constructions.hlean b/group_theory/constructions.hlean
index 5755d1b..b37014d 100644
--- a/group_theory/constructions.hlean
+++ b/group_theory/constructions.hlean
@@ -356,7 +356,7 @@ namespace group
 
   end
   end free_group open free_group
-  export [reduce_hints] free_group
+--  export [reduce_hints] free_group
   variables (X)
   definition group_free_group [constructor] : group (free_group_carrier X) :=
   group.mk free_group_mul _ free_group_mul_assoc free_group_one free_group_one_mul free_group_mul_one
diff --git a/homotopy/sample.hlean b/homotopy/sample.hlean
index f4949ae..14be533 100644
--- a/homotopy/sample.hlean
+++ b/homotopy/sample.hlean
@@ -3,7 +3,7 @@ Copyright (c) 2015 Ulrik Buchholtz. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Ulrik Buchholtz
 -/
-import types.trunc types.arrow_2 types.fiber .susp
+import types.trunc types.arrow_2 types.fiber homotopy.susp
 
 open eq is_trunc is_equiv nat equiv trunc function fiber
 
@@ -153,7 +153,7 @@ namespace homotopy
   -- Corollary 7.5.5
   definition is_conn_homotopy (n : trunc_index) {A B : Type} {f g : A → B}
     (p : f ~ g) (H : is_conn_map n f) : is_conn_map n g :=
-  @retract_of_conn_is_conn _ _ (arrow.arrow_hom_of_homotopy p) (arrow.is_retraction_arrow_hom_of_homotopy p) n H 
+  @retract_of_conn_is_conn _ _ (arrow.arrow_hom_of_homotopy p) (arrow.is_retraction_arrow_hom_of_homotopy p) n H
 
   -- all types are -2-connected
   definition minus_two_conn [instance] (A : Type) : is_conn -2 A :=