diff options
Diffstat (limited to 'extraction')
| -rw-r--r-- | extraction/extraction.v | 12 |
1 files changed, 1 insertions, 11 deletions
diff --git a/extraction/extraction.v b/extraction/extraction.v index c0286f7b..25319475 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -34,7 +34,6 @@ Require Clight. Require Compiler. Require Parser. Require Initializers. -Require Int31. (* Standard lib *) Require Import ExtrOcamlBasic. @@ -128,7 +127,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; @@ -137,15 +136,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. |