From d1cdc0496d7d52e3ab91554dbf53fcc0e7f244eb Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 17 Apr 2009 13:27:48 +0000
Subject: Various clean-ups

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1033 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 extraction/extraction.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'extraction/extraction.v')

diff --git a/extraction/extraction.v b/extraction/extraction.v
index 58da9c06..d74e192e 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -22,6 +22,7 @@ Require Compiler.
 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 => "list" [ "[]" "(::)" ].
 
 (* Float *)
@@ -82,4 +83,5 @@ Extract Constant Asm.freg_eq => "fun (x: freg) (y: freg) -> x = y".
 Extract Constant Asm.preg_eq => "fun (x: preg) (y: preg) -> x = y".
 
 (* Go! *)
+Cd "extraction".
 Recursive Extraction Library Compiler.
-- 
cgit