aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic/Core.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Arithmetic/Core.v')
-rw-r--r--src/Arithmetic/Core.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Arithmetic/Core.v b/src/Arithmetic/Core.v
index 97986091c..1309aa393 100644
--- a/src/Arithmetic/Core.v
+++ b/src/Arithmetic/Core.v
@@ -1094,7 +1094,7 @@ Ltac presolve_op_mod_eq wt x :=
| autorewrite with uncps push_id push_basesystem_eval ].
Ltac solve_op_mod_eq wt x :=
- presolve_op_mod_eq;
+ presolve_op_mod_eq wt x;
[ basesystem_partial_evaluation_RHS;
do_replace_match_with_destructuring_match_in_goal
| reflexivity ].