diff options
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index dc7522b8..aca7102d 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -42,10 +42,6 @@ Extract Inlined Constant Coqlib.proj_sumbool => "(fun x -> x)". (* Wfsimpl *) Extraction Inline Wfsimpl.Fix Wfsimpl.Fixm. -(* AST *) -Extract Constant AST.ident_of_string => - "fun s -> Camlcoq.intern_string (Camlcoq.camlstring_of_coqstring s)". - (* Memory - work around an extraction bug. *) Extraction NoInline Memory.Mem.valid_pointer. |