From cd330c1092aaf234ad3c28c14ef2ac591fa60127 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Sun, 11 Jun 2023 19:25:38 +0200
Subject: [PATCH] remove a noLoc

---
 lib/Quox/Syntax/Term/Subst.idr | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/lib/Quox/Syntax/Term/Subst.idr b/lib/Quox/Syntax/Term/Subst.idr
index 2054976..06a9a25 100644
--- a/lib/Quox/Syntax/Term/Subst.idr
+++ b/lib/Quox/Syntax/Term/Subst.idr
@@ -334,8 +334,7 @@ private %inline
 CompHY : (ty : DScopeTerm d n) -> (p, q : Dim d) -> (val : Term d n) ->
          (r : Dim d) -> (zero, one : DScopeTerm d n) -> (loc : Loc) -> Elim d n
 CompHY {ty, p, q, val, r, zero, one, loc} =
-  -- [fixme] maintain location of existing B VZ
-  let ty' = SY ty.names $ ty.term // (B VZ noLoc ::: shift 2) in
+  let ty' = SY ty.names $ ty.term // (B VZ ty.loc ::: shift 2) in
   Comp {
     ty = dsub1 ty q, p, q,
     val = E $ Coe ty p q val val.loc, r,