[ quote ] Turn off tcinlining when quoting delays

buzden · Jul 31, 2024 · a9d9919 · a9d9919
1 parent 72241a4
commit a9d9919
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/Core/Normalise/Quote.idr b/src/Core/Normalise/Quote.idr
@@ -217,7 +217,8 @@ mutual
       toHolesOnly : Closure vs -> Closure vs
       toHolesOnly (MkClosure opts locs env tm)
           = MkClosure ({ holesOnly := True,
-                         argHolesOnly := True } opts)
+                         argHolesOnly := True,
+                         tcInline := False } opts)
                       locs env tm
       toHolesOnly c = c
   quoteGenNF q opts defs bound env (NForce fc r arg args)