From 4828afa7819998a690f5bbc3e4f9a0de9bedc980 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Tue, 27 Oct 2015 23:32:12 -0400
Subject: [PATCH] fix(hott): small fixes after rebasing

---
 hott/algebra/category/nat_trans.hlean   | 2 +-
 hott/algebra/category/precategory.hlean | 2 +-
 hott/init/types.hlean                   | 4 ++--
 3 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/hott/algebra/category/nat_trans.hlean b/hott/algebra/category/nat_trans.hlean
index eb618f409c..e430ab2c13 100644
--- a/hott/algebra/category/nat_trans.hlean
+++ b/hott/algebra/category/nat_trans.hlean
@@ -182,7 +182,7 @@ namespace nat_trans
   nat_trans.mk (λc, hom_of_eq (ap010 to_fun_ob p c))
                (λa b f, eq.rec_on p (!id_right ⬝ !id_left⁻¹))
 
-  definition compose_rev [unfold-full] (θ : F ⟹ G) (η : G ⟹ H) : F ⟹ H := η ∘n θ
+  definition compose_rev [unfold_full] (θ : F ⟹ G) (η : G ⟹ H) : F ⟹ H := η ∘n θ
 
 end nat_trans
 
diff --git a/hott/algebra/category/precategory.hlean b/hott/algebra/category/precategory.hlean
index 1e11ebacba..71652857c2 100644
--- a/hott/algebra/category/precategory.hlean
+++ b/hott/algebra/category/precategory.hlean
@@ -35,7 +35,7 @@ namespace category
 
   infixr ∘ := precategory.comp
   -- input ⟶ using \--> (this is a different arrow than \-> (→))
-  infixl [parsing_only] ` ⟶ `:25 := precategory.hom
+  infixl [parsing_only] ` ⟶ `:60 := precategory.hom
   namespace hom
     infixl ` ⟶ `:60 := precategory.hom -- if you open this namespace, hom a b is printed as a ⟶ b
   end hom
diff --git a/hott/init/types.hlean b/hott/init/types.hlean
index 8bd30b1588..10adfb37ac 100644
--- a/hott/init/types.hlean
+++ b/hott/init/types.hlean
@@ -51,7 +51,7 @@ end sigma
 namespace sum
   infixr ⊎ := sum
   infixr + := sum
-  infixr [parsing-only] `+t`:25 := sum -- notation which is never overloaded
+  infixr [parsing_only] `+t`:25 := sum -- notation which is never overloaded
   namespace low_precedence_plus
     reserve infixr ` + `:25  -- conflicts with notation for addition
     infixr ` + ` := sum
@@ -84,7 +84,7 @@ namespace prod
   -- notation for n-ary tuples
   notation `(` h `, ` t:(foldl `,` (e r, prod.mk r e) h) `)` := t
   infixr × := prod
-  infixr [parsing-only] `×t`:30 := prod -- notation which is never overloaded
+  infixr [parsing_only] `×t`:30 := prod -- notation which is never overloaded
 
   namespace ops
   infixr [parsing_only] * := prod