diff options
Diffstat (limited to 'src/Util/ZUtil.v')
| -rw-r--r-- | src/Util/ZUtil.v | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index a9dcde3d9..07e9af549 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -1170,7 +1170,7 @@ Module Z. refine (proj1 (@reflect_iff_gen _ _ lem b') _); cbv beta iota. - Ltac ltb_to_lt'_hyps_step := + Ltac ltb_to_lt_hyps_step := match goal with | [ H : (?x <? ?y) = ?b |- _ ] => ltb_to_lt_with_hyp H (Zlt_cases x y) @@ -1183,7 +1183,7 @@ Module Z. | [ H : (?x =? ?y) = ?b |- _ ] => ltb_to_lt_with_hyp H (eqb_cases x y) end. - Ltac ltb_to_lt'_goal_step := + Ltac ltb_to_lt_goal_step := match goal with | [ |- (?x <? ?y) = ?b ] => ltb_to_lt_in_goal b (Z.ltb_spec0 x y) @@ -1196,13 +1196,13 @@ Module Z. | [ |- (?x =? ?y) = ?b ] => ltb_to_lt_in_goal b (Z.eqb_spec x y) end. - Ltac ltb_to_lt'_step := - first [ ltb_to_lt'_hyps_step - | ltb_to_lt'_goal_step ]. - Ltac ltb_to_lt' := repeat ltb_to_lt'_step. + Ltac ltb_to_lt_step := + first [ ltb_to_lt_hyps_step + | ltb_to_lt_goal_step ]. + Ltac ltb_to_lt := repeat ltb_to_lt_step. Section R_Rb. - Local Ltac t := intros ? ? []; split; intro; ltb_to_lt'; omega. + Local Ltac t := intros ? ? []; split; intro; ltb_to_lt; omega. Local Notation R_Rb Rb R nR := (forall x y b, Rb x y = b <-> if b then R x y else nR x y). Lemma ltb_lt_iff : R_Rb Z.ltb Z.lt Z.ge. Proof. t. Qed. Lemma leb_le_iff : R_Rb Z.leb Z.le Z.gt. Proof. t. Qed. @@ -1211,7 +1211,7 @@ Module Z. Lemma eqb_eq_iff : R_Rb Z.eqb (@Logic.eq Z) (fun x y => x <> y). Proof. t. Qed. End R_Rb. Hint Rewrite ltb_lt_iff leb_le_iff gtb_gt_iff geb_ge_iff eqb_eq_iff : ltb_to_lt. - Ltac ltb_to_lt := + Ltac ltb_to_lt_in_context := repeat autorewrite with ltb_to_lt in *; cbv beta iota in *. |