From a9e8f14ad54823257d0930e2dca6a4df1471d9df Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 21 Mar 2024 21:29:01 +0100
Subject: [PATCH] fix a small bug in Q.Whnf.Coercion

---
 lib/Quox/Whnf/Coercion.idr | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/lib/Quox/Whnf/Coercion.idr b/lib/Quox/Whnf/Coercion.idr
index c97ed91..91d94d2 100644
--- a/lib/Quox/Whnf/Coercion.idr
+++ b/lib/Quox/Whnf/Coercion.idr
@@ -199,7 +199,7 @@ parameters {auto _ : CanWhnf Term Interface.isRedexT}
             fstInSnd =
               CoeT !(fresh i)
                    (tfst // (BV 0 loc ::: shift 2))
-                   (weakD 1 p) (BV 0 loc) (dweakT 1 s) fst.loc
+                   (weakD 1 p) (BV 0 loc) (dweakT 1 fst) fst.loc
             snd' = CoeT i (sub1 tsnd fstInSnd) p q snd snd.loc
         whnf defs ctx sg $
           Ann (Pair (E fst') (E snd') sLoc) (ty // one q) loc