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. --- common/Memory.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'common/Memory.v') diff --git a/common/Memory.v b/common/Memory.v index ec436103..2c9151ed 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -1806,7 +1806,7 @@ Proof. intros. unfold load. destruct (valid_access_dec m2 chunk b' ofs Readable). exploit valid_access_alloc_inv; eauto. destruct (eq_block b' b); intros. - subst b'. elimtype False. eauto with mem. + subst b'. exfalso. eauto with mem. rewrite pred_dec_true; auto. injection ALLOC; intros. rewrite <- H2; simpl. rewrite PMap.gso. auto. rewrite H1. apply not_eq_sym; eauto with mem. @@ -1940,7 +1940,7 @@ Proof. rewrite PMap.gsspec. destruct (peq b bf). subst b. destruct (zle lo ofs); simpl. destruct (zlt ofs hi); simpl. - elimtype False; intuition. + exfalso; intuition. auto. auto. auto. Qed. -- cgit