diff --git a/Test/TestPaper.v b/Test/TestPaper.v
index 6300301..67c8112 100644
--- a/Test/TestPaper.v
+++ b/Test/TestPaper.v
@@ -333,7 +333,7 @@ vm_compute in counts4;
 pose (t3 := eval e3 __vars); 
 pose (t4 := eval e4 __vars); 
 cbv [eval nth nullary_real unary_real binary_real bpow' __vars] in t3, t4;
-elimtype False; clear - t3 t4 counts0 counts1 counts2 counts3 counts4.
+exfalso; clear - t3 t4 counts0 counts1 counts2 counts3 counts4.
 Open Scope Z.
 
 (*
diff --git a/Test/TestRefman.v b/Test/TestRefman.v
index c0508e4..1ed7b33 100644
--- a/Test/TestRefman.v
+++ b/Test/TestRefman.v
@@ -329,7 +329,7 @@ vm_compute in counts4;
 pose (t3 := eval e3 __vars); 
 pose (t4 := eval e4 __vars); 
 cbv [eval nth nullary_real unary_real binary_real bpow' __vars] in t3, t4;
-elimtype False; clear - t3 t4 counts0 counts1 counts2 counts3 counts4.
+exfalso; clear - t3 t4 counts0 counts1 counts2 counts3 counts4.
 Open Scope Z.
 
 (*
diff --git a/vcfloat/Float_lemmas.v b/vcfloat/Float_lemmas.v
index 8c86478..89593d3 100644
--- a/vcfloat/Float_lemmas.v
+++ b/vcfloat/Float_lemmas.v
@@ -246,7 +246,7 @@ Proof.
   rewrite (FF2B_gen_correct _ _ _ (F2_valid_binary _ _ H)).
   set (j := F2_valid_binary _ _ _). clearbody j. revert j.
   destruct (F2 _ _ _) eqn:?H; intros; auto;
-  elimtype False; clear - H0; unfold F2 in H0;
+  exfalso; clear - H0; unfold F2 in H0;
   destruct (Z_lt_le_dec _ _) in H0; inversion H0.
 Qed.
 
@@ -666,7 +666,7 @@ unfold B2, F2 in H0;
 destruct (Z_lt_le_dec (e + 1) (3 - femax ty)); [ | lia];
 inversion H0; auto.
 all:
-elimtype False;
+exfalso;
 unfold B2, F2 in H0;
 destruct (Z_lt_le_dec (e + 1) (3 - femax ty)); [ | lia];
 inversion H0.
diff --git a/vcfloat/Prune.v b/vcfloat/Prune.v
index fe82b1a..d939ada 100644
--- a/vcfloat/Prune.v
+++ b/vcfloat/Prune.v
@@ -577,7 +577,7 @@ match goal with |- context [F.real (F.max ?a ?b)] =>
 end].
 unfold Xcmp.
 destruct (F.toX l) eqn:Hl1. {
-  elimtype False; clear - Hl Hl1.
+  exfalso; clear - Hl Hl1.
   unfold F.toX in *.
   unfold F.toF in *.
   unfold F.classify in *.
@@ -585,7 +585,7 @@ destruct (F.toX l) eqn:Hl1. {
   destruct (FloatOps.Prim2SF l); try destruct s; simpl in *; try discriminate.
 }
 destruct (F.toX u) eqn:Hu1. {
-  elimtype False; clear - Hu Hu1.
+  exfalso; clear - Hu Hu1.
   unfold F.toX in *.
   unfold F.toF in *.
   unfold F.classify in *.