update some call following agda's warning

agda · Sep 12, 2023 · 33ce421 · 33ce421
1 parent e24f92c
commit 33ce421
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/Cubical/Tactics/Reflection.agda b/Cubical/Tactics/Reflection.agda
@@ -89,7 +89,7 @@ get-boundary tm = unapply-path tm >>= λ where
 equation-solver : List Name → (Term -> Term -> TC Term) → Bool → Term → TC Unit
 equation-solver don't-Reduce mk-call debug hole =
     withNormalisation false (
-    dontReduceDefs don't-Reduce (
+    withReduceDefs (false , don't-Reduce) (
     do
       -- | First we normalize the goal
       goal ← inferType hole >>= reduce