diff options
| author |  xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-10-18 09:40:59 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-10-18 09:40:59 +0000 |
| commit | cdcb658c29409c8aef94ca3e22c14a90b396aea0 (patch) | |
| tree | 8981d0a2312604c6b8ab8a8acb108f39f1cd1377 /extraction | |
| parent | f535ac931c2b7dc65fefa83e47bb8c79ca90e92d (diff) | |
Extraction: map Coq pairs to Caml pairs and Coq chars (type ascii) to Caml chars
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1732 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
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 4bfac69..52706ab 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -19,11 +19,8 @@ Require Compiler. Require Initializers. (* Standard lib *) -Extract Inductive unit => "unit" [ "()" ]. -Extract Inductive bool => "bool" [ "true" "false" ]. -Extract Inductive sumbool => "bool" [ "true" "false" ]. -Extract Inductive option => "option" [ "Some" "None" ]. -Extract Inductive list => "list" [ "[]" "(::)" ]. +Require Import ExtrOcamlBasic. +Require Import ExtrOcamlString. (* Float *) Extract Inlined Constant Floats.float => "float". |