diff options
author | François Pottier <francois.pottier@inria.fr> | 2015-10-23 15:08:33 +0200 |
---|---|---|
committer | François Pottier <francois.pottier@inria.fr> | 2015-10-23 15:17:50 +0200 |
commit | 136986c204af19341aeb455d72fe817b16fa6fff (patch) | |
tree | 02e9178d9f2cf942bd32366891d480ff161406f6 /extraction | |
parent | c46723c0169145d41d1879c236f53314456f1ba1 (diff) | |
parent | 1cb3d93ff278ebbd0c6967c5f9401a97f9b618b4 (diff) | |
download | compcert-136986c204af19341aeb455d72fe817b16fa6fff.tar.gz compcert-136986c204af19341aeb455d72fe817b16fa6fff.zip |
Merge remote branch 'upstream/master' into clean
Conflicts:
Makefile.extr
Diffstat (limited to 'extraction')
-rw-r--r-- | extraction/extraction.v | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index 6327f871..0f0a8637 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. @@ -115,7 +111,7 @@ Extract Constant Compiler.time => "Timing.time_coq". (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*) (* Cabs *) -Extract Constant Cabs.cabsloc => +Extract Constant Cabs.cabsloc => "{ lineno : int; filename: string; byteno: int; @@ -168,4 +164,5 @@ Separate Extraction Machregs.mregs_for_operation Machregs.mregs_for_builtin Machregs.two_address_op Machregs.is_stack_reg AST.signature_main + AST.transform_partial_ident_program Parser.translation_unit_file. |