From 4bc80f8513d05f3aceb8d052b8dd59a6b00e3e60 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 4 Jul 2011 18:05:17 +0000
Subject: Set Extraction KeepSingleton: an option for not decapsulating
 singleton types

 A informative inductive type with one constructor C and one informative arg to C
 is normally extracted as an identity, with C removed, see for example
 the "sig" type. When this new option is set, these singleton types
 are left untouch, providing extracted code which is closer to the initial
 Coq development.

 Feature requested by Wouter Swiestra.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14260 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/extraction/table.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'plugins/extraction/table.ml')

diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index aa312321b6..c58672ca0a 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -421,6 +421,10 @@ let auto_inline = my_bool_option "AutoInline" false
 
 let type_expand = my_bool_option "TypeExpand" true
 
+(*s Extraction KeepSingleton *)
+
+let keep_singleton = my_bool_option "KeepSingleton" false
+
 (*s Extraction Optimize *)
 
 type opt_flag =
-- 
cgit v1.2.3