From 9aebb168a3f9b5bf74342b1533071dd91a4100fc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 22 Jul 2016 11:36:33 -0700
Subject: [PATCH] chore(library/init/option): remove bad comment

---
 library/init/option.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/library/init/option.lean b/library/init/option.lean
index 56f144ff82..ccfa0d3e7d 100644
--- a/library/init/option.lean
+++ b/library/init/option.lean
@@ -2,8 +2,6 @@
 Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
-
-Basic datatypes
 -/
 prelude
 import init.logic init.monad init.alternative