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 /common | |
| 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 'common')
| -rw-r--r-- | common/Events.v | 2 | ||||
| -rw-r--r-- | common/Memory.v | 4 |
2 files changed, 3 insertions, 3 deletions
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. |