From 0f919eb26c68d3882e612a1b3a9df45bee6d3624 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 13 Feb 2019 18:53:17 +0100 Subject: Upgrade embedded version of Flocq to 3.1. Main changes to CompCert outside of Flocq are as follows: - Minimal supported version of Coq is now 8.7, due to Flocq requirements. - Most modifications are due to Z2R being dropped in favor of IZR and to the way Flocq now handles NaNs. - CompCert now correctly handles NaNs for the Risc-V architecture (hopefully). --- extraction/extraction.v | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index a47a7237..15a64d89 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -153,11 +153,11 @@ Load extractionMachdep. Extraction Blacklist List String Int. (* Cutting the dependency to R. *) -Extract Inlined Constant Fcore_defs.F2R => "fun _ -> assert false". -Extract Inlined Constant Fappli_IEEE.FF2R => "fun _ -> assert false". -Extract Inlined Constant Fappli_IEEE.B2R => "fun _ -> assert false". -Extract Inlined Constant Fappli_IEEE.round_mode => "fun _ -> assert false". -Extract Inlined Constant Fcalc_bracket.inbetween_loc => "fun _ -> assert false". +Extract Inlined Constant Defs.F2R => "fun _ -> assert false". +Extract Inlined Constant Binary.FF2R => "fun _ -> assert false". +Extract Inlined Constant Binary.B2R => "fun _ -> assert false". +Extract Inlined Constant Binary.round_mode => "fun _ -> assert false". +Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false". (* Needed in Coq 8.4 to avoid problems with Function definitions. *) Set Extraction AccessOpaque. -- cgit