diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-07-19 18:25:09 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-07-19 18:25:09 +0200 |
| commit | 3b79923a6c9fa8c76916df1eecfdecd7ae2124a5 (patch) | |
| tree | 98b27b88ea7195a244eff90eaa5f63028ad518a6 /extraction | |
| parent | 9bc337d05eed466e2bfc9b18aa35fac34d3954a9 (diff) | |
| parent | 91381b65f5aa76e5195caae9ef331b3f5f95afaf (diff) | |
| download | compcert-kvx-3b79923a6c9fa8c76916df1eecfdecd7ae2124a5.tar.gz compcert-kvx-3b79923a6c9fa8c76916df1eecfdecd7ae2124a5.zip | |
Merge branch 'master' of https://github.com/AbsInt/CompCert into mppa-work-upstream-merge
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 17 |
1 files changed, 6 insertions, 11 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index 265a5967..5a1ca0be 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -34,8 +34,11 @@ Require Clight. Require Compiler. Require Parser. Require Initializers. +<<<<<<< HEAD Require Int31. Require Asmaux. +======= +>>>>>>> 91381b65f5aa76e5195caae9ef331b3f5f95afaf (* Standard lib *) Require Import ExtrOcamlBasic. @@ -141,7 +144,7 @@ Extract Constant Compiler.time => "Timing.time_coq". (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*) (* Cabs *) -Extract Constant Cabs.cabsloc => +Extract Constant Cabs.loc => "{ lineno : int; filename: string; byteno: int; @@ -150,15 +153,6 @@ Extract Constant Cabs.cabsloc => Extract Inlined Constant Cabs.string => "String.t". Extract Constant Cabs.char_code => "int64". -(* Int31 *) -Extract Inductive Int31.digits => "bool" [ "false" "true" ]. -Extract Inductive Int31.int31 => "int" [ "Camlcoq.Int31.constr" ] "Camlcoq.Int31.destr". -Extract Constant Int31.twice => "Camlcoq.Int31.twice". -Extract Constant Int31.twice_plus_one => "Camlcoq.Int31.twice_plus_one". -Extract Constant Int31.compare31 => "Camlcoq.Int31.compare". -Extract Constant Int31.On => "0". -Extract Constant Int31.In => "1". - (* Processor-specific extraction directives *) Load extractionMachdep. @@ -185,9 +179,10 @@ Separate Extraction Cexec.do_initial_state Cexec.do_step Cexec.at_final_state Ctypes.merge_attributes Ctypes.remove_attributes Ctypes.build_composite_env Initializers.transl_init Initializers.constval - Csyntax.Eindex Csyntax.Epreincr + Csyntax.Eindex Csyntax.Epreincr Csyntax.Eselection Ctyping.typecheck_program Ctyping.epostincr Ctyping.epostdecr Ctyping.epreincr Ctyping.epredecr + Ctyping.eselection Ctypes.make_program Clight.type_of_function Conventions1.callee_save_type Conventions1.is_float_reg |