diff options
Diffstat (limited to 'extraction/extraction.v')
| -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. |