From c0b4a47f63dfaa6f58e752f71517a7e2393ebfaf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 24 Mar 2015 11:44:04 -0700
Subject: [PATCH] refactor(hott/algebra/precategory/functor): remove
 unnecessary annotation

---
 hott/algebra/precategory/functor.hlean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/hott/algebra/precategory/functor.hlean b/hott/algebra/precategory/functor.hlean
index 3a1f9ef2e..1aa02d6cb 100644
--- a/hott/algebra/precategory/functor.hlean
+++ b/hott/algebra/precategory/functor.hlean
@@ -123,9 +123,7 @@ namespace functor
   protected definition comp_id_eq_id_comp (F : C ⇒ D) : F ∘f functor.id = functor.id ∘f F :=
   !functor.id_right ⬝ !functor.id_left⁻¹
 
-  set_option apply.class_instance false
   -- "functor C D" is equivalent to a certain sigma type
-  set_option unifier.max_steps 38500
   protected definition sigma_char :
     (Σ (to_fun_ob : C → D)
     (to_fun_hom : Π ⦃a b : C⦄, hom a b → hom (to_fun_ob a) (to_fun_ob b)),
@@ -150,6 +148,7 @@ namespace functor
         apply idp},
   end
 
+  set_option apply.class_instance false
   protected definition is_hset_functor
     [HD : is_hset D] : is_hset (functor C D) :=
   begin