Merge pull request #19 from JasonGross/17781-compat

Stop using `elimtype False`
VeriNum · Aug 31, 2023 · 688347e · 688347e
2 parents 35a4c24 + 7afdc9d
commit 688347e
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 6 deletions.
diff --git 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
@@ -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
@@ -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
@@ -577,15 +577,15 @@ 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 *.
   rewrite FloatAxioms.classify_spec in Hl.
   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 *.