From 9aacc59135071a979623ab177819cdbe9ce27056 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 8 Sep 2020 18:29:00 +0200 Subject: Upgrade to Flocq 4.0. --- extraction/extraction.v | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) (limited to 'extraction/extraction.v') 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. *) -- cgit