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/Environment.idr | 2 ++
 1 file changed, 2 insertions(+)

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

diff --git a/src/Core/Term/Environment.idr b/src/Core/Term/Environment.idr
index 1cc7ba8..7b05ec0 100644
--- a/src/Core/Term/Environment.idr
+++ b/src/Core/Term/Environment.idr
@@ -5,6 +5,8 @@ import Core.Term
 import Core.Thinning
 import Core.Var
 
+%prefix_record_projections off
+
 -- Definition ------------------------------------------------------------------
 
 public export
-- 
cgit v1.2.3