From 9a17d567ec76fd48bb17e8da640cff606e57af42 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 3 Sep 2016 16:59:55 -0700
Subject: [PATCH] refactor(library/init/datatypes): remove notation nobody uses

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

diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean
index 8796b5741f..64096c3609 100644
--- a/library/init/datatypes.lean
+++ b/library/init/datatypes.lean
@@ -7,8 +7,6 @@ Basic datatypes
 -/
 prelude
 notation `Prop`  := Type.{0}
-notation [parsing_only] `Type'` := Type.{_+1}
-notation [parsing_only] `Type₊` := Type.{_+1}
 notation `Type₁` := Type.{1}
 notation `Type₂` := Type.{2}
 notation `Type₃` := Type.{3}