diff --git a/src/Quox/Pretty.idr b/src/Quox/Pretty.idr
index a445c79..a9296ba 100644
--- a/src/Quox/Pretty.idr
+++ b/src/Quox/Pretty.idr
@@ -137,11 +137,11 @@ public export
 interface PrettyHL a where
   prettyM : HasEnv m => a -> m (Doc HL)
 
-public export %inline
+export %inline
 pretty0M : (PrettyHL a, HasEnv m) => a -> m (Doc HL)
 pretty0M = local {prec := Outer} . prettyM
 
-public export %inline
+export %inline
 pretty0 : PrettyHL a => {default True unicode : Bool} -> a -> Doc HL
 pretty0 x {unicode} =
   let env = MakePrettyEnv {dnames = [], tnames = [], unicode, prec = Outer} in
diff --git a/src/Quox/Syntax/Shift.idr b/src/Quox/Syntax/Shift.idr
index dfee608..471f13f 100644
--- a/src/Quox/Syntax/Shift.idr
+++ b/src/Quox/Syntax/Shift.idr
@@ -49,7 +49,7 @@ toEqv Refl {by = SZ}      = EqSZ
 toEqv Refl {by = (SS by)} = EqSS $ toEqv Refl {by}
 
 
-public export
+export
 0 shiftDiff : (by : Shift from to) -> to = by.nat + from
 shiftDiff SZ      = Refl
 shiftDiff (SS by) = cong S $ shiftDiff by
diff --git a/src/Quox/Syntax/Term.idr b/src/Quox/Syntax/Term.idr
index 91efaf9..d892157 100644
--- a/src/Quox/Syntax/Term.idr
+++ b/src/Quox/Syntax/Term.idr
@@ -332,10 +332,10 @@ parameters {auto _ : Alternative f}
   upsilon1 (E e :# _) = pure e
   upsilon1 _          = empty
 
-  public export
+  export
   step : Elim d n -> f (Elim d n)
   step e = betaLam1 e <|> upsilon1 e
 
-public export
+export
 step' : Elim d n -> Elim d n
 step' e = fromMaybe e $ step e
diff --git a/src/Quox/Syntax/Var.idr b/src/Quox/Syntax/Var.idr
index 513a057..976b3d7 100644
--- a/src/Quox/Syntax/Var.idr
+++ b/src/Quox/Syntax/Var.idr
@@ -68,7 +68,7 @@ public export %inline
 V : (i : Nat) -> {auto 0 p : i `LT` n} -> Var n
 V i {p} = fromNatWith i p
 
-public export %inline
+export %inline
 tryFromNat : Alternative f => (n : Nat) -> Nat -> f (Var n)
 tryFromNat n i =
   case i `isLT` n of