Extract Inductive is now possible toward non-inductive types (e.g. nat => int)

 For instance:

  Extract Inductive nat => int [ "0" "succ" ]
   "(fun fO fS n => if n=0 then fO () else fS (n-1))".

 See Extraction.v for more details and caveat.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13025 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 1 deletions

diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 3d980e65f..137ae9047 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -219,6 +219,14 @@ let rec pp_expr par env args =
 	if str_global Cons r = "" (* hack Extract Inductive prod *)
 	then tuple
 	else pp_par par (pp_global Cons r ++ spc () ++ tuple)
+    | MLcase (_, t, pv) when is_custom_match pv ->
+	let mkfun (_,ids,e) =
+	  if ids <> [] then named_lams (List.rev ids) e
+	  else dummy_lams (ast_lift 1 e) 1
+	in
+	hov 2 (str (find_custom_match pv) ++ fnl () ++
+		 prvect (fun tr -> pp_expr true env [] (mkfun tr) ++ fnl ()) pv
+	       ++ pp_expr true env [] t)
     | MLcase ((i,factors), t, pv) ->
 	let expr = if i = Coinductive then
 	  (str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
@@ -328,7 +336,7 @@ and pp_function env t =
   let bl,t' = collect_lams t in
   let bl,env' = push_vars (List.map id_of_mlid bl) env in
   match t' with
-    | MLcase(i,MLrel 1,pv) when fst i=Standard ->
+    | MLcase(i,MLrel 1,pv) when fst i=Standard && not (is_custom_match pv) ->
 	if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then
 	  pr_binding (List.rev (List.tl bl)) ++
        	  str " = function" ++ fnl () ++