diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-11 10:48:19 -0500 |
|---|---|---|
| committer |  Jason Gross <jasongross9@gmail.com> | 2016-11-11 16:07:28 -0500 |
| commit | a15de3edd5bbbf0d2d427d815744bfd1b669bae8 (patch) | |
| tree | 6748ebfb8b6f0e54e3587683db290d50018c5925 /src | |
| parent | 12a21acfcbacbd1d9d9574e1e2523797b371de1c (diff) | |
Remove more conditional subtract
Diffstat (limited to 'src')
| -rw-r--r-- | src/Reflection/Z/Interpretations/Relations.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/Reflection/Z/Interpretations/Relations.v b/src/Reflection/Z/Interpretations/Relations.v index 3760b15e0..3e018678d 100644 --- a/src/Reflection/Z/Interpretations/Relations.v +++ b/src/Reflection/Z/Interpretations/Relations.v @@ -465,8 +465,7 @@ Local Ltac related_Z_op_fin_t_step := | [ H : context[Tuple.lift_option (Tuple.push_option _)] |- _ ] => rewrite Tuple.lift_push_option in H end - | progress Z.ltb_to_lt - | (progress unfold ZBounds.conditional_subtract in * ); break_match_hyps ]. + | progress Z.ltb_to_lt ]. Local Ltac related_Z_op_fin_t := repeat related_Z_op_fin_t_step. Local Opaque Word64.bit_width. |