diff options
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. *) |