From 77c76a43689ce532921ccfa200b44083bc52dc21 Mon Sep 17 00:00:00 2001 From: Andres Erbsen Date: Tue, 14 Feb 2023 23:05:22 -0500 Subject: [PATCH] adapt for coq/coq#17022 (#96) --- src/Rewriter/Util/ListUtil.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Rewriter/Util/ListUtil.v b/src/Rewriter/Util/ListUtil.v index 8561d5fa9..e9cb56be8 100644 --- a/src/Rewriter/Util/ListUtil.v +++ b/src/Rewriter/Util/ListUtil.v @@ -542,8 +542,8 @@ Lemma list_bl_hetero {A B} {AB_beq : A -> B -> bool} {AB_R : A -> B -> Prop} : forall {x y}, list_beq_hetero AB_beq x y = true -> list_eq AB_R x y. Proof using Type. - induction x, y; cbn in *; eauto; try congruence. - rewrite Bool.andb_true_iff; intuition eauto. + induction x, y; cbn in *; eauto; try congruence; + try (rewrite Bool.andb_true_iff; intuition eauto). Qed. Lemma list_lb_hetero {A B} {AB_beq : A -> B -> bool} {AB_R : A -> B -> Prop}