Use `exfalso` instead of `elimtype False` (#470)

Adapt w.r.t. coq/coq#16904.

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.