diff options
| author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2019-02-13 18:53:17 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-03-27 11:38:25 +0100 |
| commit | 0f919eb26c68d3882e612a1b3a9df45bee6d3624 (patch) | |
| tree | b8bcf57e06d761be09b8d2cf2f80741acb1e4949 /extraction | |
| parent | d5c0b4054c8490bda3b3d191724c58d5d4002e58 (diff) | |
| download | compcert-kvx-0f919eb26c68d3882e612a1b3a9df45bee6d3624.tar.gz compcert-kvx-0f919eb26c68d3882e612a1b3a9df45bee6d3624.zip | |
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).
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 10 |
1 files changed, 5 insertions, 5 deletions
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. |