From b514a978b2740a7d4932f65085bbf1d0f9d8eded Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Wed, 12 Nov 2014 18:01:01 -0500
Subject: [PATCH] fix(library/hott) changed pointed.lean to use trunc.lean
 correctly

---
 library/hott/pointed.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/library/hott/pointed.lean b/library/hott/pointed.lean
index 95c6c0420..d151c5f08 100644
--- a/library/hott/pointed.lean
+++ b/library/hott/pointed.lean
@@ -4,20 +4,20 @@
 -- Ported from Coq HoTT
 import hott.path hott.trunc data.sigma data.prod
 
-open path prod
+open path prod truncation
 
 inductive is_pointed [class] (A : Type) :=
   pointed_mk : Π(a : A), is_pointed A
 
 namespace is_pointed
-  variables {A B : Type} (f : A → B)
+  variables {A B : Type.{1}} (f : A → B)
 
   definition point (A : Type) [H : is_pointed A] : A :=
     is_pointed.rec (λinv, inv) H
 
   -- Any contractible type is pointed
-  protected definition contr [instance] (H : Contr A) : is_pointed A :=
-    pointed_mk (center H)
+  protected definition contr [instance] [H : is_contr A] : is_pointed A :=
+    pointed_mk (center A)
 
   -- A pi type with a pointed target is pointed
   protected definition pi [instance] {P : A → Type} [H : Πx, is_pointed (P x)]