diff --git a/hott/init/reserved_notation.hlean b/hott/init/reserved_notation.hlean
index a08fae263..abe7003d3 100644
--- a/hott/init/reserved_notation.hlean
+++ b/hott/init/reserved_notation.hlean
@@ -66,6 +66,7 @@ reserve infixl `div`:70
 reserve infixl `mod`:70
 reserve infixl `/`:70
 reserve prefix `-`:100
+reserve infix `^`:80
 
 reserve infix `<=`:50
 reserve infix `≤`:50
@@ -93,7 +94,7 @@ reserve infixl `++`:65
 reserve infixr `::`:65
 
 -- Yet another trick to anotate an expression with a type
-abbreviation is_typeof (A : Type) (a : A) : A := a
+abbreviation is_typeof [parsing-only] (A : Type) (a : A) : A := a
 
 notation `typeof` t `:` T  := is_typeof T t
 notation `(` t `:` T `)`  := is_typeof T t
diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean
index b08af371c..6ded1f13f 100644
--- a/library/init/reserved_notation.lean
+++ b/library/init/reserved_notation.lean
@@ -95,7 +95,7 @@ reserve infixl `++`:65
 reserve infixr `::`:65
 
 -- Yet another trick to anotate an expression with a type
-abbreviation is_typeof (A : Type) (a : A) : A := a
+abbreviation is_typeof [parsing-only] (A : Type) (a : A) : A := a
 
 notation `typeof` t `:` T  := is_typeof T t
 notation `(` t `:` T `)`  := is_typeof T t