From 3ba79a0e18341806007ec091940eb1b8378ab739 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@college-de-france.fr>
Date: Mon, 6 Mar 2023 17:18:55 +0100
Subject: Upgrade Flocq to 4.1.1

---
 flocq/Core/Raux.v            |  4 ++--
 flocq/Prop/Double_rounding.v | 24 ++++++++++++------------
 flocq/Version.v              |  2 +-
 3 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/flocq/Core/Raux.v b/flocq/Core/Raux.v
index 4b2ce8d7..432d3214 100644
--- a/flocq/Core/Raux.v
+++ b/flocq/Core/Raux.v
@@ -214,7 +214,7 @@ destruct (Req_dec x 0) as [Zx|Nzx].
   unfold sqrt.
   destruct Rcase_abs.
   + reflexivity.
-  + casetype False.
+  + exfalso.
     now apply Nzx, Rle_antisym; [|apply Rge_le].
 Qed.
 
@@ -2355,7 +2355,7 @@ assert (H: forall i, (i < N)%nat -> ~ P i).
   apply archimed.
 destruct (HP N) as [PN|PN].
   now split.
-elimtype False.
+exfalso.
 refine (Rle_not_lt _ _ (lub (/ (INR (S N) + 1))%R _) _).
   intros x [y [[Py ->]|[_ ->]]].
   destruct (eq_nat_dec y N) as [HyN|HyN].
diff --git a/flocq/Prop/Double_rounding.v b/flocq/Prop/Double_rounding.v
index 0580ab5e..53535b9e 100644
--- a/flocq/Prop/Double_rounding.v
+++ b/flocq/Prop/Double_rounding.v
@@ -987,7 +987,7 @@ assert (UB : y * bpow (- fexp (mag x)) < / IZR (beta ^ k)).
       * lia.
       * simpl; unfold Raux.bpow, Z.pow_pos.
         now apply Rle_refl.
-      * casetype False; apply (Z.lt_irrefl 0).
+      * exfalso; apply (Z.lt_irrefl 0).
         apply (Z.lt_trans _ _ _ Hk).
         apply Zlt_neg_0. }
 rewrite (Zfloor_imp mx).
@@ -2859,7 +2859,7 @@ destruct (Rle_or_lt x 0) as [Npx|Px].
   + now apply sqrt_lt_R0.
   + lia.
   + lia.
-  + intros Hmid; casetype False; apply (Rle_not_lt _ _ Hmid).
+  + intros Hmid; exfalso; apply (Rle_not_lt _ _ Hmid).
     apply (round_round_sqrt_aux fexp1 fexp2 Vfexp1 Vfexp2 Hexp x Px Hf2 Fx).
 Qed.
 
@@ -2978,7 +2978,7 @@ unfold round_round_sqrt_hyp; split; [|split]; intros ex.
   + destruct (Z.ltb_spec (ex - prec') emin');
     destruct (Z.ltb_spec (ex - prec) emin);
     lia.
-  + casetype False.
+  + exfalso.
     rewrite (Zlt_bool_true _ _ H') in H.
     lia.
 Qed.
@@ -3240,7 +3240,7 @@ destruct (Rle_or_lt x 0) as [Npx|Px].
       unfold sqrt.
       destruct Rcase_abs.
       + reflexivity.
-      + casetype False; lra. }
+      + exfalso; lra. }
   rewrite Hs.
   rewrite round_0.
   + reflexivity.
@@ -3288,7 +3288,7 @@ destruct (Rle_or_lt x 0) as [Npx|Px].
   + now apply sqrt_lt_R0.
   + lia.
   + lia.
-  + intros Hmid; casetype False; apply (Rle_not_lt _ _ Hmid).
+  + intros Hmid; exfalso; apply (Rle_not_lt _ _ Hmid).
     apply (round_round_sqrt_radix_ge_4_aux Hbeta fexp1 fexp2 Vfexp1 Vfexp2
                                            Hexp x Px Hf2 Fx).
 Qed.
@@ -3412,7 +3412,7 @@ unfold round_round_sqrt_radix_ge_4_hyp; split; [|split]; intros ex.
   + destruct (Z.ltb_spec (ex - prec') emin');
     destruct (Z.ltb_spec (ex - prec) emin);
     lia.
-  + casetype False.
+  + exfalso.
     rewrite (Zlt_bool_true _ _ H') in H.
     lia.
 Qed.
@@ -3605,7 +3605,7 @@ destruct (Zle_or_lt (fexp2 (mag x)) (mag x)).
       rewrite <- (Zmult_1_r beta) at 1.
       apply Zmult_lt_compat_l; lia.
 - (* mag x < fexp2 (mag x) *)
-  casetype False; apply Nzx''.
+  exfalso; apply Nzx''.
   now apply (round_N_small_pos beta _ _ _ (mag x)).
 Qed.
 
@@ -4286,16 +4286,16 @@ apply round_round_all_mid_cases.
 - exact Pxy.
 - apply Hexp.
 - intros Hf1 Hlxy.
-  casetype False.
+  exfalso.
   now apply (round_round_div_aux0 fexp1 fexp2 _ _ choice1 choice2 Hexp x y).
 - intros Hf1 Hlxy.
-  casetype False.
+  exfalso.
   now apply (round_round_div_aux1 fexp1 fexp2 _ _ choice1 choice2 Hexp x y).
 - intro H.
   apply round_round_eq_mid_beta_even; try assumption.
   apply Hexp.
 - intros Hf1 Hlxy.
-  casetype False.
+  exfalso.
   now apply (round_round_div_aux2 fexp1 fexp2 _ _ choice1 choice2 Hexp x y).
 Qed.
 
@@ -4331,7 +4331,7 @@ destruct (Rtotal_order x 0) as [Nx|[Zx|Px]].
     apply generic_format_opp in Fy.
     now apply round_round_div_aux.
   + (* y = 0 *)
-    now casetype False; apply Nzy.
+    now exfalso; apply Nzy.
   + (* y > 0 *)
     rewrite <- (Ropp_involutive x).
     rewrite Ropp_div.
@@ -4358,7 +4358,7 @@ destruct (Rtotal_order x 0) as [Nx|[Zx|Px]].
     apply generic_format_opp in Fy.
     now apply round_round_div_aux.
   + (* y = 0 *)
-    now casetype False; apply Nzy.
+    now exfalso; apply Nzy.
   + (* y > 0 *)
     now apply round_round_div_aux.
 Qed.
diff --git a/flocq/Version.v b/flocq/Version.v
index 8f1a4eae..5ff408dd 100644
--- a/flocq/Version.v
+++ b/flocq/Version.v
@@ -29,4 +29,4 @@ Definition Flocq_version := Eval vm_compute in
       parse t major (minor * 10 + N_of_ascii h - N_of_ascii "0"%char)%N
     | Empty_string => (major * 100 + minor)%N
     end in
-  parse "4.1.0"%string N0 N0.
+  parse "4.1.1"%string N0 N0.
-- 
cgit