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 +- backend/RTLgenproof.v | 4 ++-- common/Events.v | 2 +- common/Memory.v | 4 ++-- lib/Iteration.v | 2 +- 5 files changed, 7 insertions(+), 7 deletions(-) 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. diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 90f03c1c..fc765ce5 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -54,11 +54,11 @@ Proof. intros until r0. repeat rewrite PTree.gsspec. destruct (peq id1 name); destruct (peq id2 name). congruence. - intros. inv H. elimtype False. + intros. inv H. exfalso. apply valid_fresh_absurd with r0 s1. apply H1. left; exists id2; auto. eauto with rtlg. - intros. inv H2. elimtype False. + intros. inv H2. exfalso. apply valid_fresh_absurd with r0 s1. apply H1. left; exists id1; auto. eauto with rtlg. diff --git a/common/Events.v b/common/Events.v index 2e076523..1b70ecd6 100644 --- a/common/Events.v +++ b/common/Events.v @@ -199,7 +199,7 @@ Program Definition split_traceinf' (t: trace) (T: traceinf') (NE: t <> E0): even | e :: t' => (e, Econsinf' t' T _) end. Next Obligation. - elimtype False. elim NE. auto. + exfalso. elim NE. auto. Qed. Next Obligation. red; intro; subst; intuition eauto. 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. diff --git a/lib/Iteration.v b/lib/Iteration.v index 66bb3970..34471826 100644 --- a/lib/Iteration.v +++ b/lib/Iteration.v @@ -240,7 +240,7 @@ Lemma iter_monot: Proof. induction p; intros. simpl. red; intros; red; auto. - destruct q. elimtype False; lia. + destruct q. exfalso; lia. simpl. apply F_iter_monot. apply IHp. lia. Qed. -- cgit