From 49c1f0ce5d39aa4ebe386ef1876b5d573e2ae4c4 Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Thu, 12 Sep 2024 22:02:56 -0700 Subject: [PATCH] better FC --- src/Lib/Check.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lib/Check.idr b/src/Lib/Check.idr index 59e1145..f5cc13f 100644 --- a/src/Lib/Check.idr +++ b/src/Lib/Check.idr @@ -222,7 +222,7 @@ insert : (ctx : Context) -> Tm -> Val -> M (Tm, Val) insert ctx tm ty = do case !(forceMeta ty) of VPi fc x Implicit a b => do - m <- freshMeta ctx fc + m <- freshMeta ctx (getFC tm) mv <- eval ctx.env CBN m insert ctx (App emptyFC tm m) !(b $$ mv) va => pure (tm, va)