From bed9467315d4e3039235ae2704c2423009dc4a6f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 29 Nov 2014 08:55:47 -0800 Subject: [PATCH] chore(library/hott/trunc): remove `set_option` --- library/hott/trunc.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/library/hott/trunc.lean b/library/hott/trunc.lean index 6240c4c70..e984e777d 100644 --- a/library/hott/trunc.lean +++ b/library/hott/trunc.lean @@ -211,7 +211,6 @@ namespace truncation definition equiv_preserves_contr (f : A → B) [Hf : is_equiv f] [HA: is_contr A] : (is_contr B) := is_contr.mk (f (center A)) (λp, moveR_M f !contr) - set_option elaborator.trace_instances true theorem contr_equiv (H : A ≃ B) [HA: is_contr A] : is_contr B := @equiv_preserves_contr _ _ (to_fun H) (to_is_equiv H) _