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

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

diff --git a/src/Core/Var.idr b/src/Core/Var.idr
index 29c6476..a16b47e 100644
--- a/src/Core/Var.idr
+++ b/src/Core/Var.idr
@@ -3,6 +3,8 @@ module Core.Var
 import Core.Context
 import Core.Thinning
 
+%prefix_record_projections off
+
 -- Variables -------------------------------------------------------------------
 
 data IsVar : Nat -> Context -> Type where
-- 
cgit v1.2.3