From 53ff29fda182629b9fd284b196ad67a47c95a777 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Sat, 1 Apr 2023 13:51:46 +0100
Subject: Fix record projection annotations.

---
 src/Core/Term.idr | 2 --
 1 file changed, 2 deletions(-)

(limited to 'src/Core/Term.idr')

diff --git a/src/Core/Term.idr b/src/Core/Term.idr
index ee61c88..930e68f 100644
--- a/src/Core/Term.idr
+++ b/src/Core/Term.idr
@@ -4,8 +4,6 @@ import Core.Context
 import Core.Var
 import Core.Thinning
 
-%prefix_record_projections off
-
 -- Definition ------------------------------------------------------------------
 
 public export
-- 
cgit v1.2.3