diff options
| author | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2015-10-11 09:56:49 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2015-10-11 09:56:49 +0200 |
| commit | f8bc6863f72948b8041289e200ff1d8b1f63a342 (patch) | |
| tree | b0c0d0713140069f6a5da2cce1296c6e275e9b4d /flocq/Core/Fcore_rnd.v | |
| parent | b0c47e12f2bbff0905ad853b90169df16d87f6be (diff) | |
| parent | 0af966a42eb60e9af43f9a450d924758a83946c6 (diff) | |
| download | compcert-f8bc6863f72948b8041289e200ff1d8b1f63a342.tar.gz compcert-f8bc6863f72948b8041289e200ff1d8b1f63a342.zip | |
Merge pull request #55 from silene/master
Upgrade to Flocq 2.5.0.
Diffstat (limited to 'flocq/Core/Fcore_rnd.v')
| -rw-r--r-- | flocq/Core/Fcore_rnd.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/flocq/Core/Fcore_rnd.v b/flocq/Core/Fcore_rnd.v index 94c94203..171c27fc 100644 --- a/flocq/Core/Fcore_rnd.v +++ b/flocq/Core/Fcore_rnd.v @@ -39,7 +39,7 @@ exists f. intros g Hg. now apply H2 with (3 := Rle_refl x). (* . *) -exists (projT1 (completeness _ H3 H1)). +exists (proj1_sig (completeness _ H3 H1)). destruct completeness as (f1, (H4, H5)). simpl. destruct H1 as (f2, H1). @@ -58,7 +58,7 @@ Theorem round_fun_of_pred : { f : R -> R | forall x, rnd x (f x) }. Proof. intros rnd H. -exists (fun x => projT1 (round_val_of_pred rnd H x)). +exists (fun x => proj1_sig (round_val_of_pred rnd H x)). intros x. now destruct round_val_of_pred as (f, H1). Qed. |