From 42c118612330317cdf0da5115f7076d56c38ff3c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Tue, 30 May 2023 12:20:03 +0200 Subject: [PATCH] Fix compilation with Coq master A goal is solved with master but I guess not with whatever version you tested. See also https://github.com/coq/coq/issues/17660 --- backend/ValueDomain.v | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index d0a66e2489..30aabe5a02 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -1129,11 +1129,13 @@ Qed. Lemma ge_vincl: forall v w, vge v w -> vincl w v = true. Proof. induction 1; simpl; try (apply andb_true_intro; split); auto using ge_pincl, proj_sumbool_is_true. + (* Coq 8.18 solves this goal automatically in the previous tactics, + with previous versions we need to solve it explicitly. *) + 5: try solve [unfold proj_sumbool; rewrite zle_true by auto; auto]. - apply is_uns_zero_ext in H0; rewrite H0. auto using proj_sumbool_is_true. - unfold proj_sumbool; rewrite zle_true by auto. auto. - unfold proj_sumbool; rewrite zle_true by lia. auto. - apply is_sgn_sign_ext in H0; auto. rewrite H0. auto using proj_sumbool_is_true. -- unfold proj_sumbool; rewrite zlt_true by auto. auto. - unfold proj_sumbool; rewrite zle_true by lia. auto. - unfold proj_sumbool; rewrite zlt_true by lia. auto. Qed.