diff --git a/Repl.lean b/Repl.lean
index ce6a9df..6a03cbe 100644
--- a/Repl.lean
+++ b/Repl.lean
@@ -5,8 +5,6 @@ namespace Pantograph.Repl
 
 open Lean
 
-set_option trace.Pantograph.Frontend.MetaTranslate true
-
 structure Context where
   coreContext : Core.Context
 
@@ -30,7 +28,7 @@ instance : MonadEnv MainM where
   getEnv := return (← get).env
   modifyEnv f := modify fun s => { s with env := f s.env  }
 
-def newGoalState (goalState: GoalState) : MainM Nat := do
+def newGoalState (goalState : GoalState) : MainM Nat := do
   let state ← get
   let stateId := state.nextId
   set { state with
diff --git a/Test/Tactic/Prograde.lean b/Test/Tactic/Prograde.lean
index 6a806ce..aace238 100644
--- a/Test/Tactic/Prograde.lean
+++ b/Test/Tactic/Prograde.lean
@@ -131,10 +131,6 @@ def test_define_root_expr : TestT Elab.TermElabM Unit := do
   let .some rootExpr := state4.rootExpr? | addTest $ assertUnreachable "Root expr"
   addTest $ LSpec.check "root" ((toString $ ← Meta.ppExpr rootExpr) = "fun p x =>\n  let binder := x.fst;\n  binder 5")
 
---set_option pp.all true
---#check @PSigma (α := Prop) (β := λ (p: Prop) => p)
---def test_define_root_expr : TestT Elab.TermElabM Unit := do
-
 def test_have_proof : TestT Elab.TermElabM Unit := do
   let rootExpr ← parseSentence "∀ (p q: Prop), p → ((p ∨ q) ∨ (p ∨ q))"
   let state0 ← GoalState.create rootExpr