Wait for goal type in Nat solver (#1263)

ncfavier · web-flow · commit fe7b50e50dd8 · 2025-10-04T23:15:34.000+02:00
diff --git a/Cubical/Tactics/NatSolver/Reflection.agda b/Cubical/Tactics/NatSolver/Reflection.agda
@@ -129,6 +129,7 @@ private
     do
       goal ← inferType hole >>= normalise
 
+      wait-for-type goal
       just (lhs , rhs) ← get-boundary goal
         where
           nothing
