From 2af8ee20eaae47102aa933014567df84a2409536 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 21 May 2023 20:10:09 +0200
Subject: [PATCH] those were not meant to stay there

---
 lib/Quox/Syntax/Term/Pretty.idr | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/lib/Quox/Syntax/Term/Pretty.idr b/lib/Quox/Syntax/Term/Pretty.idr
index d9c20fb..112185c 100644
--- a/lib/Quox/Syntax/Term/Pretty.idr
+++ b/lib/Quox/Syntax/Term/Pretty.idr
@@ -221,9 +221,6 @@ where
     go (Left  p :: xs) $ assert_smaller e $ pushSubsts' f
   go xs s = (s, xs)
 
-export FromString (Elim d n) where fromString s = F (fromString s) noLoc
-export FromString (Term d n) where fromString s = FT (fromString s) noLoc
-
 private
 prettyDTApps : {opts : _} ->
                BContext d -> BContext n ->