diff options
Diffstat (limited to 'extraction/extraction.v')
| -rw-r--r-- | extraction/extraction.v | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index 2319be17..621298f8 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -144,18 +144,6 @@ Load extractionMachdep. (* Avoid name clashes *) Extraction Blacklist List String Int. -(* Cutting the dependency to R. *) -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 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. *) Set Extraction AccessOpaque. |