From 6029f130782e4c64cdda796351f0bebf9330a732 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Sun, 28 May 2023 01:19:27 +0200 Subject: [PATCH] Fix compilation on Coq master. --- backend/ValueDomain.v | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/backend/ValueDomain.v b/backend/ValueDomain.v index d0a66e2489..3c54ed04cf 100644 --- a/backend/ValueDomain.v +++ b/backend/ValueDomain.v @@ -1129,13 +1129,10 @@ 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. + all: try (unfold proj_sumbool; rewrite zle_true by lia; auto). + all: try (unfold proj_sumbool; rewrite zlt_true by lia; 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. (** Loading constants *)