From 0af966a42eb60e9af43f9a450d924758a83946c6 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 22 Sep 2015 15:41:50 +0200 Subject: Upgrade to Flocq 2.5.0. Note: this version of Flocq is compatible with both Coq 8.4 and 8.5. --- flocq/Core/Fcore_rnd.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'flocq/Core/Fcore_rnd.v') 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. -- cgit