From 51125c1577d0cc598a2b3413fee036a036a8a45e Mon Sep 17 00:00:00 2001 From: Soonho Kong Date: Fri, 24 Oct 2014 07:40:50 -0700 Subject: [PATCH] fix(library/data/quotient/default.lean): remove classical --- library/data/quotient/default.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/data/quotient/default.lean b/library/data/quotient/default.lean index 22d38eec9..9c1431474 100644 --- a/library/data/quotient/default.lean +++ b/library/data/quotient/default.lean @@ -2,4 +2,4 @@ --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Jeremy Avigad -import .basic .classical +import .basic