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