diff options
Diffstat (limited to 'extraction/extraction.v')
| -rw-r--r-- | extraction/extraction.v | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index 8c2a52a2..621298f8 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -144,13 +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 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. |