diff options
| author |  Jason Gross <jagro@google.com> | 2016-07-01 09:13:52 -0700 |
|---|---|---|
| committer | Jason Gross <jagro@google.com> | 2016-07-01 09:13:52 -0700 |
| commit | cb75fd18fba514577fb465d84e31ae9c6787bcd1 (patch) | |
| tree | aa1aaf8b5c0fdd9ffeff3996302be3f66d34c5cf /src/Util/ZUtil.v | |
| parent | 4cb63acdb7ea7e98d124274fec85d1a10d86d38d (diff) | |
Fix a typo in Zsplit_sums
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index 84d9ed3da..095d418a8 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -546,7 +546,7 @@ Ltac Zsplit_sums_step := => etransitivity; [ eapply Z.sub_le_mono | ] end. Ltac Zsplit_sums := - try (Zsplit_sums_step; [ Zsplit_sums | ]). + try (Zsplit_sums_step; [ Zsplit_sums.. | ]). Ltac Zpre_reorder_fractions_step := match goal with | [ |- context[?x / ?y * ?z] ] |