From fc79b13a30f124e9ac2d658773c395e0a74e2d1e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 22 Dec 2022 16:20:15 +0100 Subject: Use `exfalso` instead of `elimtype False` (#470) Adapt w.r.t. coq/coq#16904. --- backend/Inliningproof.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'backend/Inliningproof.v') diff --git a/backend/Inliningproof.v b/backend/Inliningproof.v index 0434a4a4..e165016a 100644 --- a/backend/Inliningproof.v +++ b/backend/Inliningproof.v @@ -721,7 +721,7 @@ Proof. eapply agree_regs_incr; eauto. eapply range_private_invariant; eauto. intros. exploit Mem.perm_alloc_inv; eauto. destruct (eq_block b0 b); intros. - subst b0. rewrite H2 in H5; inv H5. elimtype False; extlia. + subst b0. rewrite H2 in H5; inv H5. exfalso; extlia. rewrite H3 in H5; auto. Qed. -- cgit