From cdcb658c29409c8aef94ca3e22c14a90b396aea0 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 18 Oct 2011 09:40:59 +0000 Subject: 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 --- extraction/extraction.v | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) (limited to 'extraction') 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". -- cgit v1.2.3