aboutsummaryrefslogtreecommitdiff
path: root/src/Arithmetic
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-10-14 17:55:28 -0400
committerGravatar Jason Gross <jgross@mit.edu>2017-10-14 17:55:28 -0400
commitbe88f27f77311ccab62d15d33a7000d6eb1c7bf3 (patch)
tree413fc4cfaba1707204ed852eb7c25d976182a9e1 /src/Arithmetic
parent933562afe15d37fa95f0b20810e47e683dc384fb (diff)
Fix a typo in the previous commit
Diffstat (limited to 'src/Arithmetic')
-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 ].