summaryrefslogtreecommitdiff
path: root/src/Core/Term/Environment.idr
diff options
context:
space:
mode:
Diffstat (limited to 'src/Core/Term/Environment.idr')
-rw-r--r--src/Core/Term/Environment.idr2
1 files changed, 2 insertions, 0 deletions
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