diff options
| author | letouzey | 2011-07-04 18:05:17 +0000 |
|---|---|---|
| committer | letouzey | 2011-07-04 18:05:17 +0000 |
| commit | 4bc80f8513d05f3aceb8d052b8dd59a6b00e3e60 (patch) | |
| tree | 2c6ccbb12bbae750782ca8542a1fb62316040617 /plugins/extraction/extraction.ml | |
| parent | 44160f6e16c9597b203e13e10f45dc346c96b1d3 (diff) | |
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
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 455965af42..8433bf9d2c 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -402,7 +402,8 @@ and extract_ind env kn = (* kn is supposed to be in long form *) if Array.length p.ip_types <> 1 then raise (I Standard); let typ = p.ip_types.(0) in let l = List.filter (fun t -> not (isDummy (expand env t))) typ in - if List.length l = 1 && not (type_mem_kn kn (List.hd l)) + if not (keep_singleton ()) && + List.length l = 1 && not (type_mem_kn kn (List.hd l)) then raise (I Singleton); if l = [] then raise (I Standard); if not mib.mind_record then raise (I Standard); |