From a15de3edd5bbbf0d2d427d815744bfd1b669bae8 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 11 Nov 2016 10:48:19 -0500 Subject: Remove more conditional subtract --- src/Reflection/Z/Interpretations/Relations.v | 3 +-- 1 file changed, 1 insertion(+), 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. -- cgit v1.2.3