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/ocaml.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'plugins/extraction/ocaml.ml') diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 902e8bbb3..f34bcf1e9 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -126,7 +126,8 @@ let rec pp_type par vl t = | Tglob (r,[a1;a2]) when is_infix r -> pp_par par (pp_rec true a1 ++ str (get_infix r) ++ pp_rec true a2) | Tglob (r,[]) -> pp_global Type r - | Tglob (IndRef(kn,0),l) when kn = mk_ind "Coq.Init.Specif" "sig" -> + | Tglob (IndRef(kn,0),l) + when not (keep_singleton ()) && kn = mk_ind "Coq.Init.Specif" "sig" -> pp_tuple_light pp_rec l | Tglob (r,l) -> pp_tuple_light pp_rec l ++ spc () ++ pp_global Type r -- cgit v1.2.3