diff options
| author | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2020-09-08 18:29:00 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@college-de-france.fr> | 2022-04-25 16:38:45 +0200 |
| commit | 9aacc59135071a979623ab177819cdbe9ce27056 (patch) | |
| tree | 1d2069eba895833fdb3a7647c3cc37cea32a0de6 /extraction/extraction.v | |
| parent | fb1f4545dfe861ff4d02816e295021a7e3061687 (diff) | |
| download | compcert-9aacc59135071a979623ab177819cdbe9ce27056.tar.gz compcert-9aacc59135071a979623ab177819cdbe9ce27056.zip | |
Upgrade to Flocq 4.0.
Diffstat (limited to 'extraction/extraction.v')
| -rw-r--r-- | extraction/extraction.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index 8c2a52a2..2319be17 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -148,7 +148,12 @@ Extraction Blacklist List String Int. 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 BinarySingleNaN.round_mode => "fun _ -> assert false". +Extract Inlined Constant BinarySingleNaN.SF2R => "fun _ -> assert false". +Extract Inlined Constant BinarySingleNaN.B2R => "fun _ -> assert false". +Extract Inlined Constant Binary.BSN.round_mode => "fun _ -> assert false". +Extract Inlined Constant Binary.BSN.SF2R => "fun _ -> assert false". +Extract Inlined Constant Binary.BSN.B2R => "fun _ -> assert false". Extract Inlined Constant Bracket.inbetween_loc => "fun _ -> assert false". (* Needed in Coq 8.4 to avoid problems with Function definitions. *) |