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