Fix 8.4{pl1,pl2} builds

1 files changed, 1 insertions, 1 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index 33b2d7f2d..7c171faf7 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -132,7 +132,7 @@ Section Carries.
     change @nth_default with @nth_default_opt in *.
     change @set_nth with @set_nth_opt in *.
     lazymatch goal with
-    | [ |- _ = _ (if ?br then ?c else ?d) ]
+    | [ |- _ = ?f (if ?br then ?c else ?d) ]
       => let x := fresh "x" in let y := fresh "y" in evar (x:digits); evar (y:digits); transitivity (if br then x else y); subst x; subst y
     end.
     2:cbv zeta.