From 1bce6b0f9f8cd614038a6e7fc21fb984724204a4 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Mon, 29 Dec 2008 13:12:08 +0000
Subject: Extract Coq lists to Caml lists.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@929 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 extraction/.depend      | 4 ++--
 extraction/extraction.v | 2 ++
 2 files changed, 4 insertions(+), 2 deletions(-)

(limited to 'extraction')

diff --git a/extraction/.depend b/extraction/.depend
index 83dc5dc..a8ae227 100644
--- a/extraction/.depend
+++ b/extraction/.depend
@@ -59,9 +59,9 @@
 ../caml/PrintPPC.cmx: PPC.cmx Datatypes.cmx ../caml/Camlcoq.cmx CList.cmx \
     AST.cmx ../caml/PrintPPC.cmi 
 ../caml/RTLgenaux.cmo: Switch.cmi Integers.cmi Datatypes.cmi CminorSel.cmi \
-    ../caml/Camlcoq.cmo CList.cmi 
+    ../caml/Camlcoq.cmo 
 ../caml/RTLgenaux.cmx: Switch.cmx Integers.cmx Datatypes.cmx CminorSel.cmx \
-    ../caml/Camlcoq.cmx CList.cmx 
+    ../caml/Camlcoq.cmx 
 ../caml/RTLtypingaux.cmo: Registers.cmi RTL.cmi Op.cmi Maps.cmi Datatypes.cmi \
     ../caml/Camlcoq.cmo CList.cmi AST.cmi 
 ../caml/RTLtypingaux.cmx: Registers.cmx RTL.cmx Op.cmx Maps.cmx Datatypes.cmx \
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 69034bc..cdb1fd6 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -10,6 +10,7 @@
 (*                                                                     *)
 (* *********************************************************************)
 
+Require List.
 Require Iteration.
 Require Floats.
 Require RTLgen.
@@ -21,6 +22,7 @@ Require Main.
 Extract Inductive unit => "unit" [ "()" ].
 Extract Inductive bool => "bool" [ "true" "false" ].
 Extract Inductive sumbool => "bool" [ "true" "false" ].
+Extract Inductive List.list => "list" [ "[]" "(::)" ].
 
 (* Float *)
 Extract Inlined Constant Floats.float => "float".
-- 
cgit v1.2.3