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/RTLgenproof.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'backend/RTLgenproof.v') 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. -- cgit