diff options
| author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2022-12-22 16:20:15 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-12-22 16:20:15 +0100 |
| commit | fc79b13a30f124e9ac2d658773c395e0a74e2d1e (patch) | |
| tree | f81eb0494f192d3abe40c7ce50a4bf77c9596766 /backend | |
| parent | 8d21a7fa245637b684ddb4c12f4bfa6295569fb6 (diff) | |
| download | compcert-fc79b13a30f124e9ac2d658773c395e0a74e2d1e.tar.gz compcert-fc79b13a30f124e9ac2d658773c395e0a74e2d1e.zip | |
Use `exfalso` instead of `elimtype False` (#470)
Adapt w.r.t. coq/coq#16904.
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Inliningproof.v | 2 | ||||
| -rw-r--r-- | backend/RTLgenproof.v | 4 |
2 files changed, 3 insertions, 3 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. |