From 9348701a5b0a141cc0aabb9223574c0e8e03565b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 18 Oct 2015 16:14:12 -0700
Subject: [PATCH] fix(library/logic/examples/instances_test): we do not support
 the `set_option class.conservative false` anymore

---
 library/logic/examples/instances_test.lean | 5 -----
 1 file changed, 5 deletions(-)

diff --git a/library/logic/examples/instances_test.lean b/library/logic/examples/instances_test.lean
index c0181cb1f..1b8888e4c 100644
--- a/library/logic/examples/instances_test.lean
+++ b/library/logic/examples/instances_test.lean
@@ -14,11 +14,6 @@ open eq.ops
 
 example (a b : Prop) (H : a ↔ b) (H1 : a) : b := mp H H1
 
-set_option class.conservative false
-
-example (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=
-subst iff H1 H2
-
 /-
 exit
 example (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) :=