diff options
| author | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2023-03-06 17:18:55 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2023-03-10 18:54:45 +0100 |
| commit | 3ba79a0e18341806007ec091940eb1b8378ab739 (patch) | |
| tree | 14ff24b4a44e33a5607f6c97b953805511b8eb27 /flocq/Core/Raux.v | |
| parent | 2c2dabd4f7b7f330cc8e6c9cf879618a422316e8 (diff) | |
| download | compcert-3ba79a0e18341806007ec091940eb1b8378ab739.tar.gz compcert-3ba79a0e18341806007ec091940eb1b8378ab739.zip | |
Upgrade Flocq to 4.1.1
Diffstat (limited to 'flocq/Core/Raux.v')
| -rw-r--r-- | flocq/Core/Raux.v | 4 |
1 files changed, 2 insertions, 2 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]. |