Extraction: Richer patterns in matchs as proposed by P.N. Tollitte

 The MLcase has notably changed:
  - No more case_info in it, but only a type annotation
  - No more "one branch for one constructor", but rather a sequence
    of patterns. Earlier "full" pattern correspond to pattern Pusual.
    Patterns Pwild and Prel allow to encode optimized matchs without
    hacks as earlier. Other pattern situations aren't used (yet)
    by extraction, but only by P.N Tollitte's code.

 A MLtuple constructor has been introduced. It isn't used by
 the extraction for the moment, but only but P.N. Tollitte's code.

 Many pretty-print functions in ocaml.ml and other have been reorganized

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

13 files changed, 535 insertions, 371 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 66ec446f0..0bd5b8434 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -33,17 +33,41 @@ let is_mp_bound = function MPbound _ -> true | _ -> false
 
 let pp_par par st = if par then str "(" ++ st ++ str ")" else st
 
+(** [pp_apply] : a head part applied to arguments, possibly with parenthesis *)
+
 let pp_apply st par args = match args with
   | [] -> st
   | _  -> hov 2 (pp_par par (st ++ spc () ++ prlist_with_sep spc identity args))
 
+(** Same as [pp_apply], but with also protection of the head by parenthesis *)
+
+let pp_apply2 st par args =
+  let par' = args <> [] || par in
+  pp_apply (pp_par par' st) par args
+
 let pr_binding = function
   | [] -> mt ()
   | l  -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
 
+let pp_tuple_light f = function
+  | [] -> mt ()
+  | [x] -> f true x
+  | l ->
+      pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) (f false) l)
+
+let pp_tuple f = function
+  | [] -> mt ()
+  | [x] -> f x
+  | l -> pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) f l)
+
+let pp_boxed_tuple f = function
+  | [] -> mt ()
+  | [x] -> f x
+  | l -> pp_par true (hov 0 (prlist_with_sep (fun () -> str "," ++ spc ()) f l))
+
 (** By default, in module Format, you can do horizontal placing of blocks
     even if they include newlines, as long as the number of chars in the
-    blocks are less that a line length. To avoid this awkward situation,
+    blocks is less that a line length. To avoid this awkward situation,
     we attach a big virtual size to [fnl] newlines. *)
 
 let fnl () = stras (1000000,"") ++ fnl ()
@@ -348,12 +372,13 @@ let ref_renaming_fun (k,r) =
   let l = mp_renaming mp in
   let l = if lang () <> Ocaml && not (modular ()) then [""] else l in
   let s =
+    let idg = safe_basename_of_global r in
     if l = [""] (* this happens only at toplevel of the monolithic case *)
     then
       let globs = Idset.elements (get_global_ids ()) in
-      let id = next_ident_away (kindcase_id k (safe_basename_of_global r)) globs in
+      let id = next_ident_away (kindcase_id k idg) globs in
       string_of_id id
-    else modular_rename k (safe_basename_of_global r)
+    else modular_rename k idg
   in
   add_global_ids (id_of_string s);
   s::l
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 1d8fe77ab..02a496bec 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -22,7 +22,17 @@ val fnl2 : unit -> std_ppcmds
 val space_if : bool -> std_ppcmds
 
 val pp_par : bool -> std_ppcmds -> std_ppcmds
+
+(** [pp_apply] : a head part applied to arguments, possibly with parenthesis *)
 val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds
+
+(** Same as [pp_apply], but with also protection of the head by parenthesis *)
+val pp_apply2 : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds
+
+val pp_tuple_light : (bool -> 'a -> std_ppcmds) -> 'a list -> std_ppcmds
+val pp_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+val pp_boxed_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+
 val pr_binding : identifier list -> std_ppcmds
 
 val rename_id : identifier -> Idset.t -> identifier
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 70783b4f9..e587bf212 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -20,3 +20,8 @@ val extraction_library : bool -> identifier -> unit
 
 val mono_environment :
  global_reference list -> module_path list -> Miniml.ml_structure
+
+(* Used by the Relation Extraction plugin *)
+
+val print_one_decl :
+  Miniml.ml_structure -> module_path -> Miniml.ml_decl -> unit
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index b780b64bb..549830fe7 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -476,6 +476,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	     ind_equiv = equiv }
     in
     add_ind kn mib i;
+    add_inductive_kind kn i.ind_kind;
     i
 
 (*s [extract_type_cons] extracts the type of an inductive
@@ -572,6 +573,8 @@ let rec extract_term env mle mlt c args =
     | LetIn (n, c1, t1, c2) ->
 	let id = id_of_name n in
 	let env' = push_rel (Name id, Some c1, t1) env in
+	(* We directly push the args inside the [LetIn].
+           TODO: the opt_let_app flag is supposed to prevent that *)
 	let args' = List.map (lift 1) args in
 	(try
 	  check_default env t1;
@@ -735,8 +738,8 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
 	| Tglob (_,l) -> List.map type_simpl l
 	| _ -> assert false
       in
-      let info = {c_kind = mi.ind_kind; c_typs = typeargs} in
-      put_magic_if magic1 (MLcons (info, ConstructRef cp, mla))
+      let typ = Tglob(IndRef ip, typeargs) in
+      put_magic_if magic1 (MLcons (typ, ConstructRef cp, mla))
   in
   (* Different situations depending of the number of arguments: *)
   if la < params_nb then
@@ -800,22 +803,22 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	(* We suppress dummy arguments according to signature. *)
 	let ids,e = case_expunge s e in
 	let e' = handle_exn r (List.length s) (fun _ -> Anonymous) e in
-	(r, List.rev ids, e')
+	(List.rev ids, Pusual r, e')
       in
       if mi.ind_kind = Singleton then
 	begin
 	  (* Informative singleton case: *)
 	  (* [match c with C i -> t] becomes [let i = c' in t'] *)
 	  assert (br_size = 1);
-	  let (_,ids,e') = extract_branch 0 in
+	  let (ids,_,e') = extract_branch 0 in
 	  assert (List.length ids = 1);
 	  MLletin (tmp_id (List.hd ids),a,e')
 	end
       else
 	(* Standard case: we apply [extract_branch]. *)
 	let typs = List.map type_simpl (Array.to_list metas) in
-	let info = { m_kind = mi.ind_kind; m_typs = typs; m_same = BranchNone }
-	in MLcase (info, a, Array.init br_size extract_branch)
+	let typ = Tglob (IndRef ip,typs) in
+	MLcase (typ, a, Array.init br_size extract_branch)
 
 (*s Extraction of a (co)-fixpoint. *)
 
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 32ad45c93..96731ed27 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -111,8 +111,8 @@ let expr_needs_par = function
 
 
 let rec pp_expr par env args =
-  let par' = args <> [] || par
-  and apply st = pp_apply st par args in
+  let apply st = pp_apply st par args
+  and apply2 st = pp_apply2 st par args in
   function
     | MLrel n ->
 	let id = get_db_name n env in apply (pr_id id)
@@ -123,7 +123,7 @@ let rec pp_expr par env args =
       	let fl,a' = collect_lams a in
 	let fl,env' = push_vars (List.map id_of_mlid fl) env in
 	let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in
-	apply (pp_par par' st)
+	apply2 st
     | MLletin (id,a1,a2) ->
 	let i,env' = push_vars [id_of_mlid id] env in
 	let pp_id = pr_id (List.hd i)
@@ -133,37 +133,42 @@ let rec pp_expr par env args =
 	  str "let {" ++ cut () ++
 	  hov 1 (pp_id ++ str " = " ++ pp_a1 ++ str "}")
 	in
-	apply
-	  (pp_par par'
-	     (hv 0 (hv 0 (hv 1 pp_def ++ spc () ++ str "in") ++
-		    spc () ++ hov 0 pp_a2)))
+	apply2 (hv 0 (hv 0 (hv 1 pp_def ++ spc () ++ str "in") ++
+		       spc () ++ hov 0 pp_a2))
     | MLglob r ->
 	apply (pp_global Term r)
-    | MLcons _ as c when is_native_char c -> assert (args=[]); pp_native_char c
-    | MLcons (_,r,[]) ->
-	assert (args=[]); pp_global Cons r
-    | MLcons (_,r,[a]) ->
-	assert (args=[]);
-	pp_par par (pp_global Cons r ++ spc () ++ pp_expr true env [] a)
-    | MLcons (_,r,args') ->
-	assert (args=[]);
-	pp_par par (pp_global Cons r ++ spc () ++
-		    prlist_with_sep spc (pp_expr true env []) args')
+    | MLcons (_,r,a) as c ->
+        assert (args=[]);
+        begin match a with
+	  | _ when is_native_char c -> pp_native_char c
+	  | [] -> pp_global Cons r
+	  | [a] ->
+	    pp_par par (pp_global Cons r ++ spc () ++ pp_expr true env [] a)
+	  | _ ->
+	    pp_par par (pp_global Cons r ++ spc () ++
+			prlist_with_sep spc (pp_expr true env []) a)
+	end
+    | MLtuple l ->
+        assert (args=[]);
+        pp_boxed_tuple (pp_expr true env []) l
     | MLcase (_,t, pv) when is_custom_match pv ->
-	let mkfun (_,ids,e) =
+        if not (is_regular_match pv) then
+	  error "Cannot mix yet user-given match and general patterns.";
+	let mkfun (ids,_,e) =
 	  if ids <> [] then named_lams (List.rev ids) e
 	  else dummy_lams (ast_lift 1 e) 1
 	in
-	apply
-	  (pp_par par'
-	     (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 (info,t, pv) ->
-      	apply (pp_par par'
-		 (v 0 (str "case " ++ pp_expr false env [] t ++ str " of {" ++
-		       fnl () ++ pp_pat env info pv)))
+	let pp_branch tr = pp_expr true env [] (mkfun tr) ++ fnl () in
+	let inner =
+	  str (find_custom_match pv) ++ fnl () ++
+	  prvect pp_branch pv ++
+	  pp_expr true env [] t
+	in
+	apply2 (hov 2 inner)
+    | MLcase (typ,t,pv) ->
+        apply2
+	  (v 0 (str "case " ++ pp_expr false env [] t ++ str " of {" ++
+		fnl () ++ pp_pat env pv))
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
       	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
@@ -176,44 +181,31 @@ let rec pp_expr par env args =
 	pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args)
     | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"")
 
-and pp_pat env info pv =
-  let pp_one_pat (name,ids,t) =
-    let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
-    let par = expr_needs_par t in
-    hov 2 (str " " ++ pp_global Cons name ++
-	   (match ids with
-	      | [] -> mt ()
-	      | _  -> (str " " ++
-		       prlist_with_sep spc pr_id (List.rev ids))) ++
-	   str " ->" ++ spc () ++ pp_expr par env' [] t)
-  in
-  let factor_br, factor_set = try match info.m_same with
-    | BranchFun ints ->
-        let i = Intset.choose ints in
-	branch_as_fun info.m_typs pv.(i), ints
-    | BranchCst ints ->
-        let i = Intset.choose ints in
-        ast_pop (branch_as_cst pv.(i)), ints
-    | BranchNone -> MLdummy, Intset.empty
-  with _ -> MLdummy, Intset.empty
-  in
-  let last = Array.length pv - 1 in
+and pp_cons_pat par r ppl =
+  pp_par par
+    (pp_global Cons r ++ space_if (ppl<>[]) ++ prlist_with_sep spc identity ppl)
+
+and pp_gen_pat par ids env = function
+  | Pcons (r,l) -> pp_cons_pat par r (List.map (pp_gen_pat true ids env) l)
+  | Pusual r -> pp_cons_pat par r (List.map pr_id ids)
+  | Ptuple l -> pp_boxed_tuple (pp_gen_pat false ids env) l
+  | Pwild -> str "_"
+  | Prel n -> pr_id (get_db_name n env)
+
+and pp_one_pat env (ids,p,t) =
+  let ids',env' = push_vars (List.rev_map id_of_mlid ids) env in
+  hov 2 (str " " ++
+	 pp_gen_pat false (List.rev ids') env' p ++
+	 str " ->" ++ spc () ++
+	 pp_expr (expr_needs_par t) env' [] t)
+
+and pp_pat env pv =
   prvecti
-    (fun i x -> if Intset.mem i factor_set then mt () else
-       (pp_one_pat pv.(i) ++
-       if i = last && Intset.is_empty factor_set then str "}" else
-	 (str ";" ++ fnl ()))) pv
-  ++
-  if Intset.is_empty factor_set then mt () else
-  let par = expr_needs_par factor_br in
-  match info.m_same with
-    | BranchFun _ ->
-        let ids, env' = push_vars [anonymous_name] env in
-        hov 2 (str " " ++ pr_id (List.hd ids) ++ str " ->" ++ spc () ++
-	       pp_expr par env' [] factor_br ++ str "}")
-    | BranchCst _ ->
-        hov 2 (str " _ ->" ++ spc () ++ pp_expr par env [] factor_br ++ str "}")
-    | BranchNone -> mt ()
+    (fun i x ->
+       pp_one_pat env pv.(i) ++
+       if i = Array.length pv - 1 then str "}" else
+	 (str ";" ++ fnl ()))
+    pv
 
 (*s names of the functions ([ids]) are already pushed in [env],
     and passed here just for convenience. *)
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index edff48c85..0bf1ff952 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -97,28 +97,17 @@ type ml_ident =
   | Tmp of identifier
 
 (** We now store some typing information on constructors
-    and cases to avoid type-unsafe optimisations.
-    For cases, we also store the set of branches to merge
-    in a common pattern, either "_ -> c" or "x -> f x"
+    and cases to avoid type-unsafe optimisations. This will be
+    either the type of the applied constructor or the type
+    of the head of the match.
 *)
 
-type constructor_info = {
-  c_kind : inductive_kind;
-  c_typs : ml_type list;
-}
-
-type branch_same =
-  | BranchNone
-  | BranchFun of Intset.t
-  | BranchCst of Intset.t
+(** Nota : the constructor [MLtuple] and the extension of [MLcase]
+    to general patterns have been proposed by P.N. Tollitte for
+    his Relation Extraction plugin. [MLtuple] is currently not
+    used by the main extraction, as well as deep patterns. *)
 
-type match_info = {
-  m_kind : inductive_kind;
-  m_typs : ml_type list;
-  m_same : branch_same
-}
-
-type ml_branch = global_reference * ml_ident list * ml_ast
+type ml_branch = ml_ident list * ml_pattern * ml_ast
 
 and ml_ast =
   | MLrel    of int
@@ -126,14 +115,22 @@ and ml_ast =
   | MLlam    of ml_ident * ml_ast
   | MLletin  of ml_ident * ml_ast * ml_ast
   | MLglob   of global_reference
-  | MLcons   of constructor_info * global_reference * ml_ast list
-  | MLcase   of match_info * ml_ast * ml_branch array
+  | MLcons   of ml_type * global_reference * ml_ast list
+  | MLtuple  of ml_ast list
+  | MLcase   of ml_type * ml_ast * ml_branch array
   | MLfix    of int * identifier array * ml_ast array
   | MLexn    of string
   | MLdummy
   | MLaxiom
   | MLmagic  of ml_ast
 
+and ml_pattern =
+  | Pcons   of global_reference * ml_pattern list
+  | Ptuple  of ml_pattern list
+  | Prel    of int (** Cf. the idents in the branch. [Prel 1] is the last one. *)
+  | Pwild
+  | Pusual  of global_reference (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **)
+
 (*s ML declarations. *)
 
 type ml_decl =
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 8a0d1a05f..5cef4764d 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -359,54 +359,61 @@ let ast_iter_rel f =
     | MLlam (_,a) -> iter (n+1) a
     | MLletin (_,a,b) -> iter n a; iter (n+1) b
     | MLcase (_,a,v) ->
-	iter n a; Array.iter (fun (_,l,t) -> iter (n + (List.length l)) t) v
+	iter n a; Array.iter (fun (l,_,t) -> iter (n + (List.length l)) t) v
     | MLfix (_,ids,v) -> let k = Array.length ids in Array.iter (iter (n+k)) v
     | MLapp (a,l) -> iter n a; List.iter (iter n) l
-    | MLcons (_,_,l) ->  List.iter (iter n) l
+    | MLcons (_,_,l) | MLtuple l ->  List.iter (iter n) l
     | MLmagic a -> iter n a
     | MLglob _ | MLexn _ | MLdummy | MLaxiom -> ()
   in iter 0
 
 (*s Map over asts. *)
 
-let ast_map_case f (c,ids,a) = (c,ids,f a)
+let ast_map_branch f (c,ids,a) = (c,ids,f a)
+
+(* Warning: in [ast_map] we assume that [f] does not change the type
+   of [MLcons] and of [MLcase] heads *)
 
 let ast_map f = function
   | MLlam (i,a) -> MLlam (i, f a)
   | MLletin (i,a,b) -> MLletin (i, f a, f b)
-  | MLcase (i,a,v) -> MLcase (i,f a, Array.map (ast_map_case f) v)
+  | MLcase (typ,a,v) -> MLcase (typ,f a, Array.map (ast_map_branch f) v)
   | MLfix (i,ids,v) -> MLfix (i, ids, Array.map f v)
   | MLapp (a,l) -> MLapp (f a, List.map f l)
-  | MLcons (i,c,l) -> MLcons (i,c, List.map f l)
+  | MLcons (typ,c,l) -> MLcons (typ,c, List.map f l)
+  | MLtuple l -> MLtuple (List.map f l)
   | MLmagic a -> MLmagic (f a)
   | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a
 
 (*s Map over asts, with binding depth as parameter. *)
 
-let ast_map_lift_case f n (c,ids,a) = (c,ids, f (n+(List.length ids)) a)
+let ast_map_lift_branch f n (ids,p,a) = (ids,p, f (n+(List.length ids)) a)
+
+(* Same warning as for [ast_map]... *)
 
 let ast_map_lift f n = function
   | MLlam (i,a) -> MLlam (i, f (n+1) a)
   | MLletin (i,a,b) -> MLletin (i, f n a, f (n+1) b)
-  | MLcase (i,a,v) -> MLcase (i,f n a,Array.map (ast_map_lift_case f n) v)
+  | MLcase (typ,a,v) -> MLcase (typ,f n a,Array.map (ast_map_lift_branch f n) v)
   | MLfix (i,ids,v) ->
       let k = Array.length ids in MLfix (i,ids,Array.map (f (k+n)) v)
   | MLapp (a,l) -> MLapp (f n a, List.map (f n) l)
-  | MLcons (i,c,l) -> MLcons (i,c, List.map (f n) l)
+  | MLcons (typ,c,l) -> MLcons (typ,c, List.map (f n) l)
+  | MLtuple l -> MLtuple (List.map (f n) l)
   | MLmagic a -> MLmagic (f n a)
   | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a
 
 (*s Iter over asts. *)
 
-let ast_iter_case f (c,ids,a) = f a
+let ast_iter_branch f (c,ids,a) = f a
 
 let ast_iter f = function
   | MLlam (i,a) -> f a
   | MLletin (i,a,b) -> f a; f b
-  | MLcase (_,a,v) -> f a; Array.iter (ast_iter_case f) v
+  | MLcase (_,a,v) -> f a; Array.iter (ast_iter_branch f) v
   | MLfix (i,ids,v) -> Array.iter f v
   | MLapp (a,l) -> f a; List.iter f l
-  | MLcons (_,c,l) -> List.iter f l
+  | MLcons (_,_,l) | MLtuple l -> List.iter f l
   | MLmagic a -> f a
   | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom  -> ()
 
@@ -436,13 +443,13 @@ let nb_occur_match =
     | MLcase(_,a,v) ->
         (nb k a) +
 	Array.fold_left
-	  (fun r (_,ids,a) -> max r (nb (k+(List.length ids)) a)) 0 v
+	  (fun r (ids,_,a) -> max r (nb (k+(List.length ids)) a)) 0 v
     | MLletin (_,a,b) -> (nb k a) + (nb (k+1) b)
     | MLfix (_,ids,v) -> let k = k+(Array.length ids) in
       Array.fold_left (fun r a -> r+(nb k a)) 0 v
     | MLlam (_,a) -> nb (k+1) a
     | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l
-    | MLcons (_,_,l) -> List.fold_left (fun r a -> r+(nb k a)) 0 l
+    | MLcons (_,_,l) | MLtuple l -> List.fold_left (fun r a -> r+(nb k a)) 0 l
     | MLmagic a -> nb k a
     | MLglob _ | MLexn _ | MLdummy | MLaxiom -> 0
   in nb 1
@@ -502,6 +509,39 @@ let gen_subst v d t =
     | a -> ast_map_lift subst n a
   in subst 0 t
 
+(*S Operations concerning match patterns *)
+
+let is_basic_pattern = function
+  | Prel _ | Pwild -> true
+  | Pusual _ | Pcons _ | Ptuple _ -> false
+
+let has_deep_pattern br =
+  let deep = function
+    | Pcons (_,l) | Ptuple l -> not (List.for_all is_basic_pattern l)
+    | Pusual _ | Prel _ | Pwild -> false
+  in
+  array_exists (function (_,pat,_) -> deep pat) br
+
+let is_regular_match br =
+  if Array.length br <> 0 then false (* empty match becomes MLexn *)
+  else
+    try
+      let get_r (ids,pat,c) =
+	match pat with
+	  | Pusual r -> r
+	  | Pcons (r,l) ->
+	    if not (list_for_all_i (fun i -> (=) (Prel i)) 1 (List.rev l))
+	    then raise Impossible;
+	    r
+	  | _ -> raise Impossible
+      in
+      let ind = match get_r br.(0) with
+	| ConstructRef (ind,_) -> ind
+	| _ -> raise Impossible
+      in
+      array_for_all_i (fun i tr -> get_r tr = ConstructRef (ind,i+1)) 0 br
+    with Impossible -> false
+
 (*S Operations concerning lambdas. *)
 
 (*s [collect_lams MLlam(id1,...MLlam(idn,t)...)] returns
@@ -650,26 +690,31 @@ let rec ast_glob_subst s t = match t with
    expansion of type definitions.
 *)
 
-(*s [branch_as_function b typs (r,l,c)] tries to see branch [c]
+(*s [branch_as_function b typ (l,p,c)] tries to see branch [c]
   as a function [f] applied to [MLcons(r,l)]. For that it transforms
   any [MLcons(r,l)] in [MLrel 1] and raises [Impossible]
   if any variable in [l] occurs outside such a [MLcons] *)
 
-let branch_as_fun typs (r,l,c) =
+let branch_as_fun typ (l,p,c) =
   let nargs = List.length l in
+  let cons = match p with
+    | Pusual r -> MLcons (typ, r, eta_args nargs)
+    | Pcons (r,pl) ->
+      let pat2rel = function Prel i -> MLrel i | _ -> raise Impossible in
+      MLcons (typ, r, List.map pat2rel pl)
+    | _ -> raise Impossible
+  in
   let rec genrec n = function
     | MLrel i as c ->
 	let i' = i-n in
 	if i'<1 then c
 	else if i'>nargs then MLrel (i-nargs+1)
 	else raise Impossible
-    | MLcons(i,r',args) when
-	r=r' && (test_eta_args_lift n nargs args) && typs = i.c_typs ->
-	MLrel (n+1)
+    | MLcons _ as cons' when cons' = ast_lift n cons -> MLrel (n+1)
     | a -> ast_map_lift genrec n a
   in genrec 0 c
 
-(*s [branch_as_cst (r,l,c)] tries to see branch [c] as a constant
+(*s [branch_as_cst (l,p,c)] tries to see branch [c] as a constant
    independent from the pattern [MLcons(r,l)]. For that is raises [Impossible]
    if any variable in [l] occurs in [c], and otherwise returns [c] lifted to
    appear like a function with one arg (for uniformity with [branch_as_fun]).
@@ -677,7 +722,7 @@ let branch_as_fun typs (r,l,c) =
    empty, i.e. when [r] is a constant constructor
 *)
 
-let branch_as_cst (_,l,c) =
+let branch_as_cst (l,_,c) =
   let n = List.length l in
   if ast_occurs_itvl 1 n c then raise Impossible;
   ast_lift (1-n) c
@@ -716,20 +761,27 @@ let census_add, census_max, census_clean =
    constant.
 *)
 
-let factor_branches o typs br =
-  census_clean ();
-  for i = 0 to Array.length br - 1 do
-    if o.opt_case_idr then
-      (try census_add (branch_as_fun typs br.(i)) i with Impossible -> ());
-    if o.opt_case_cst then
-      (try census_add (branch_as_cst br.(i)) i with Impossible -> ());
-  done;
-  let br_factor, br_set = census_max MLdummy in
-  census_clean ();
-  let n = Intset.cardinal br_set in
-  if n = 0 then None
-  else if Array.length br >= 2 && n < 2 then None
-  else Some (br_factor, br_set)
+let is_opt_pat (_,p,_) = match p with
+  | Prel _ | Pwild -> true
+  | _ -> false
+
+let factor_branches o typ br =
+  if array_exists is_opt_pat br then None (* already optimized *)
+  else begin
+    census_clean ();
+    for i = 0 to Array.length br - 1 do
+      if o.opt_case_idr then
+	(try census_add (branch_as_fun typ br.(i)) i with Impossible -> ());
+      if o.opt_case_cst then
+	(try census_add (branch_as_cst br.(i)) i with Impossible -> ());
+    done;
+    let br_factor, br_set = census_max MLdummy in
+    census_clean ();
+    let n = Intset.cardinal br_set in
+    if n = 0 then None
+    else if Array.length br >= 2 && n < 2 then None
+    else Some (br_factor, br_set)
+  end
 
 (*s If all branches are functions, try to permut the case and the functions. *)
 
@@ -752,14 +804,14 @@ let rec permut_case_fun br acc =
     let br = Array.copy br in
     let ids = ref [] in
     for i = 0 to Array.length br - 1 do
-      let (r,l,t) = br.(i) in
+      let (l,p,t) = br.(i) in
       let local_nb = nb_lams t in
       if local_nb < !nb then (* t = MLexn ... *)
-	br.(i) <- (r,l,remove_n_lams local_nb t)
+	br.(i) <- (l,p,remove_n_lams local_nb t)
       else begin
 	let local_ids,t = collect_n_lams !nb t in
 	ids := merge_ids !ids local_ids;
-	br.(i) <- (r,l,permut_rels !nb (List.length l) t)
+	br.(i) <- (l,p,permut_rels !nb (List.length l) t)
       end
     done;
     (!ids,br)
@@ -767,32 +819,43 @@ let rec permut_case_fun br acc =
 
 (*S Generalized iota-reduction. *)
 
-(* Definition of a generalized iota-redex: it's a [MLcase(e,_)]
-   with [(is_iota_gen e)=true]. Any generalized iota-redex is
-   transformed into beta-redexes. *)
-
-let rec is_iota_gen = function
-  | MLcons _ -> true
-  | MLcase(_,_,br)-> array_for_all (fun (_,_,t)->is_iota_gen t) br
-  | _ -> false
-
-let constructor_index = function
-  | ConstructRef (_,j) -> pred j
-  | _ -> assert false
-
-let iota_gen br =
+(* Definition of a generalized iota-redex: it's a [MLcase(e,br)]
+   where the head [e] is a [MLcons] or made of [MLcase]'s with
+   [MLcons] as leaf branches.
+   A generalized iota-redex is transformed into beta-redexes. *)
+
+(* In [iota_red], we try to simplify a [MLcase(_,MLcons(typ,r,a),br)].
+   Argument [i] is the branch we consider, we should lift what
+   comes from [br] by [lift] *)
+
+let rec iota_red i lift br ((typ,r,a) as cons) =
+  if i >= Array.length br then raise Impossible;
+  let (ids,p,c) = br.(i) in
+  match p with
+    | Pusual r' | Pcons (r',_) when r'<>r -> iota_red (i+1) lift br cons
+    | Pusual r' ->
+      let c = named_lams (List.rev ids) c in
+      let c = ast_lift lift c
+      in MLapp (c,a)
+    | Prel 1 when List.length ids = 1 ->
+      let c = MLlam (List.hd ids, c) in
+      let c = ast_lift lift c
+      in MLapp(c,[MLcons(typ,r,a)])
+    | Pwild when ids = [] -> ast_lift lift c
+    | _ -> raise Impossible (* TODO: handle some more cases *)
+
+(* [iota_gen] is an extension of [iota_red] where we allow to
+   traverse matches in the head of the first match *)
+
+let iota_gen br hd =
   let rec iota k = function
-    | MLcons (i,r,a) ->
-	let (_,ids,c) = br.(constructor_index r) in
-	let c = List.fold_right (fun id t -> MLlam (id,t)) ids c in
-	let c = ast_lift k c in
-	MLapp (c,a)
-    | MLcase(i,e,br') ->
+    | MLcons (typ,r,a) -> iota_red 0 k br (typ,r,a)
+    | MLcase(typ,e,br') ->
 	let new_br =
-	  Array.map (fun (n,i,c)->(n,i,iota (k+(List.length i)) c)) br'
-	in MLcase(i,e, new_br)
-    | _ -> assert false
-  in iota 0
+	  Array.map (fun (i,p,c)->(i,p,iota (k+(List.length i)) c)) br'
+	in MLcase(typ,e,new_br)
+    | _ -> raise Impossible
+  in iota 0 hd
 
 let is_atomic = function
   | MLrel _ | MLglob _ | MLexn _ | MLdummy -> true
@@ -824,9 +887,9 @@ let expand_linear_let o id e =
 let rec simpl o = function
   | MLapp (f, []) -> simpl o f
   | MLapp (f, a) -> simpl_app o (List.map (simpl o) a) (simpl o f)
-  | MLcase (i,e,br) ->
-      let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in
-      simpl_case o i br (simpl o e)
+  | MLcase (typ,e,br) ->
+      let br = Array.map (fun (l,p,t) -> (l,p,simpl o t)) br in
+      simpl_case o typ br (simpl o e)
   | MLletin(Dummy,_,e) -> simpl o (ast_pop e)
   | MLletin(id,c,e) ->
       let e = simpl o e in
@@ -862,40 +925,50 @@ and simpl_app o a = function
   | MLletin (id,e1,e2) when o.opt_let_app ->
       (* Application of a letin: we push arguments inside *)
       MLletin (id, e1, simpl o (MLapp (e2, List.map (ast_lift 1) a)))
-  | MLcase (i,e,br) when o.opt_case_app ->
+  | MLcase (typ,e,br) when o.opt_case_app ->
       (* Application of a case: we push arguments inside *)
       let br' =
 	Array.map
-      	  (fun (n,l,t) ->
+	  (fun (l,p,t) ->
 	     let k = List.length l in
 	     let a' = List.map (ast_lift k) a in
-      	     (n, l, simpl o (MLapp (t,a')))) br
-      in simpl o (MLcase (i,e,br'))
+	     (l, p, simpl o (MLapp (t,a')))) br
+      in simpl o (MLcase (typ,e,br'))
   | (MLdummy | MLexn _) as e -> e
 	(* We just discard arguments in those cases. *)
   | f -> MLapp (f,a)
 
 (* Invariant : all empty matches should now be [MLexn] *)
 
-and simpl_case o i br e =
-  if o.opt_case_iot && (is_iota_gen e) then (* Generalized iota-redex *)
+and simpl_case o typ br e =
+  try
+    (* Generalized iota-redex *)
+    if not o.opt_case_iot then raise Impossible;
     simpl o (iota_gen br e)
-  else
+  with Impossible ->
     (* Swap the case and the lam if possible *)
     let ids,br = if o.opt_case_fun then permut_case_fun br [] else [],br in
     let n = List.length ids in
     if n <> 0 then
-      simpl o (named_lams ids (MLcase (i,ast_lift n e, br)))
+      simpl o (named_lams ids (MLcase (typ, ast_lift n e, br)))
     else
       (* Can we merge several branches as the same constant or function ? *)
-      match factor_branches o i.m_typs br with
+      if lang() = Scheme || is_custom_match br
+      then MLcase (typ, e, br)
+      else match factor_branches o typ br with
 	| Some (f,ints) when Intset.cardinal ints = Array.length br ->
-	    (* If all branches have been factorized, we remove the match *)
-	    simpl o (MLletin (Tmp anonymous_name, e, f))
+	  (* If all branches have been factorized, we remove the match *)
+	  simpl o (MLletin (Tmp anonymous_name, e, f))
 	| Some (f,ints) ->
-	  let same = if ast_occurs 1 f then BranchFun ints else BranchCst ints
-	  in MLcase ({i with m_same=same}, e, br)
-	| None -> MLcase (i, e, br)
+	  let last_br =
+	    if ast_occurs 1 f then ([Tmp anonymous_name], Prel 1, f)
+	    else ([], Pwild, ast_pop f)
+	  in
+	  let brl = Array.to_list br in
+	  let brl_opt = list_filter_i (fun i _ -> not (Intset.mem i ints)) brl in
+	  let brl_opt = brl_opt @ [last_br] in
+	  MLcase (typ, e, Array.of_list brl_opt)
+	| None -> MLcase (typ, e, br)
 
 (*S Local prop elimination. *)
 (* We try to eliminate as many [prop] as possible inside an [ml_ast]. *)
@@ -1107,20 +1180,21 @@ let optimize_fix a =
 
 (* Utility functions used in the decision of inlining. *)
 
+let ml_size_branch size pv = Array.fold_left (fun a (_,_,t) -> a + size t) 0 pv
+
 let rec ml_size = function
   | MLapp(t,l) -> List.length l + ml_size t + ml_size_list l
   | MLlam(_,t) -> 1 + ml_size t
-  | MLcons(_,_,l) -> ml_size_list l
-  | MLcase(_,t,pv) ->
-      1 + ml_size t + (Array.fold_right (fun (_,_,t) a -> a + ml_size t) pv 0)
+  | MLcons(_,_,l) | MLtuple l -> ml_size_list l
+  | MLcase(_,t,pv) -> 1 + ml_size t + ml_size_branch ml_size pv
   | MLfix(_,_,f) -> ml_size_array f
   | MLletin (_,_,t) -> ml_size t
   | MLmagic t -> ml_size t
-  | _ -> 0
+  | MLglob _ | MLrel _ | MLexn _ | MLdummy | MLaxiom -> 0
 
 and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l
 
-and ml_size_array l = Array.fold_left (fun a t -> a + ml_size t) 0 l
+and ml_size_array a = Array.fold_left (fun a t -> a + ml_size t) 0 a
 
 let is_fix = function MLfix _ -> true | _ -> false
 
@@ -1172,7 +1246,7 @@ let rec non_stricts add cand = function
       (* so we make an union (in fact a merge). *)
       let cand = non_stricts false cand t in
       Array.fold_left
-	(fun c (_,i,t)->
+	(fun c (i,_,t)->
 	   let n = List.length i in
 	   let cand = lift n cand in
 	   let cand = pop n (non_stricts add cand t) in
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index e8fa9c47b..452fd46c0 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -113,9 +113,11 @@ val normalize : ml_ast -> ml_ast
 val optimize_fix : ml_ast -> ml_ast
 val inline : global_reference -> ml_ast -> bool
 
+val is_basic_pattern : ml_pattern -> bool
+val has_deep_pattern : ml_branch array -> bool
+val is_regular_match : ml_branch array -> bool
+
 exception Impossible
-val branch_as_fun : ml_type list -> ml_branch -> ml_ast
-val branch_as_cst : ml_branch -> ml_ast
 
 (* Classification of signatures *)
 
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index a548c7866..9e8dd8286 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -77,18 +77,26 @@ let type_iter_references do_type t =
     | _ -> ()
   in iter t
 
+let patt_iter_references do_cons p =
+  let rec iter = function
+    | Pcons (r,l) -> do_cons r; List.iter iter l
+    | Pusual r -> do_cons r
+    | Ptuple l -> List.iter iter l
+    | Prel _ | Pwild -> ()
+  in iter p
+
 let ast_iter_references do_term do_cons do_type a =
   let rec iter a =
     ast_iter iter a;
     match a with
       | MLglob r -> do_term r
-      | MLcons (i,r,_) ->
-	  if lang () = Ocaml then record_iter_references do_term i.c_kind;
-	  do_cons r
-      | MLcase (i,_,v) ->
-	  if lang () = Ocaml then record_iter_references do_term i.m_kind;
-	  Array.iter (fun (r,_,_) -> do_cons r) v
-      | _ -> ()
+      | MLcons (_,r,_) -> do_cons r
+      | MLcase (ty,_,v) ->
+	type_iter_references do_type ty;
+	Array.iter (fun (_,p,_) -> patt_iter_references do_cons p) v
+
+      | MLrel _ | MLlam _ | MLapp _ | MLletin _ | MLtuple _ | MLfix _ | MLexn _
+      | MLdummy | MLaxiom | MLmagic _ -> ()
   in iter a
 
 let ind_iter_references do_term do_cons do_type kn ind =
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 9885c64b1..ed69ec457 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -29,22 +29,6 @@ let pp_tvar id =
   then str ("'"^s)
   else str ("' "^s)
 
-let pp_tuple_light f = function
-  | [] -> mt ()
-  | [x] -> f true x
-  | l ->
-      pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) (f false) l)
-
-let pp_tuple f = function
-  | [] -> mt ()
-  | [x] -> f x
-  | l -> pp_par true (prlist_with_sep (fun () -> str "," ++ spc ()) f l)
-
-let pp_boxed_tuple f = function
-  | [] -> mt ()
-  | [x] -> f x
-  | l -> pp_par true (hov 0 (prlist_with_sep (fun () -> str "," ++ spc ()) f l))
-
 let pp_abst = function
   | [] -> mt ()
   | l  ->
@@ -57,6 +41,10 @@ let pp_parameters l =
 let pp_string_parameters l =
   (pp_boxed_tuple str l ++ space_if (l<>[]))
 
+let pp_letin pat def body =
+  let fstline = str "let " ++ pat ++ str " =" ++ spc () ++ def in
+  hv 0 (hv 0 (hov 2 fstline ++ spc () ++ str "in") ++ spc () ++ hov 0 body)
+
 (*s Ocaml renaming issues. *)
 
 let keywords =
@@ -153,10 +141,19 @@ let rec pp_type par vl t =
     de Bruijn variables. [args] is the list of collected arguments
     (already pretty-printed). *)
 
+let is_bool_patt p s =
+  try
+    let r = match p with
+      | Pusual r -> r
+      | Pcons (r,[]) -> r
+      | _ -> raise Not_found
+    in
+    find_custom r = s
+  with Not_found -> false
+
+
 let is_ifthenelse = function
-  | [|(r1,[],_);(r2,[],_)|] ->
-      (try (find_custom r1 = "true") && (find_custom r2 = "false")
-       with Not_found -> false)
+  | [|([],p1,_);([],p2,_)|] -> is_bool_patt p1 "true" && is_bool_patt p2 "false"
   | _ -> false
 
 let expr_needs_par = function
@@ -166,8 +163,8 @@ let expr_needs_par = function
   | _        -> false
 
 let rec pp_expr par env args =
-  let par' = args <> [] || par
-  and apply st = pp_apply st par args in
+  let apply st = pp_apply st par args
+  and apply2 st = pp_apply2 st par args in
   function
     | MLrel n ->
 	let id = get_db_name n env in apply (pr_id id)
@@ -178,109 +175,23 @@ let rec pp_expr par env args =
       	let fl,a' = collect_lams a in
 	let fl = List.map id_of_mlid fl in
 	let fl,env' = push_vars fl env in
-	let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in
-	apply (pp_par par' st)
+	let st = pp_abst (List.rev fl) ++ pp_expr false env' [] a' in
+	apply2 st
     | MLletin (id,a1,a2) ->
 	let i,env' = push_vars [id_of_mlid id] env in
 	let pp_id = pr_id (List.hd i)
 	and pp_a1 = pp_expr false env [] a1
 	and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
-	hv 0
-	  (apply
-	     (pp_par par'
-		(hv 0
-		   (hov 2
-		      (str "let " ++ pp_id ++ str " =" ++ spc () ++ pp_a1) ++
-		    spc () ++ str "in") ++
-		 spc () ++ hov 0 pp_a2)))
+	hv 0 (apply2 (pp_letin pp_id pp_a1 pp_a2))
     | MLglob r ->
 	(try
 	   let args = list_skipn (projection_arity r) args in
 	   let record = List.hd args in
 	   pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args)
 	 with _ -> apply (pp_global Term r))
-    | MLcons _ as c when is_native_char c -> assert (args=[]); pp_native_char c
-    | MLcons ({c_kind = Coinductive},r,[]) ->
-	assert (args=[]);
-	pp_par par (str "lazy " ++ pp_global Cons r)
-    | MLcons ({c_kind = Coinductive},r,args') ->
-	assert (args=[]);
-	let tuple = pp_tuple (pp_expr true env []) args' in
-	pp_par par (str "lazy (" ++ pp_global Cons r ++ spc() ++ tuple ++str ")")
-    | MLcons (_,r,[]) ->
-	assert (args=[]);
-	pp_global Cons r
-    | MLcons ({c_kind = Record fields}, r, args') ->
-	assert (args=[]);
-	pp_record_pat (pp_fields r fields, List.map (pp_expr true env []) args')
-    | MLcons (_,r,[arg1;arg2]) when is_infix r ->
-	assert (args=[]);
-	pp_par par
-	  ((pp_expr true env [] arg1) ++ str (get_infix r) ++
-	   (pp_expr true env [] arg2))
-    | MLcons (_,r,args') ->
-	assert (args=[]);
-	let tuple = pp_tuple (pp_expr true env []) args' in
-	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
-	apply
-	  (pp_par par'
-	     (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 (info, t, pv) ->
-	let expr = if info.m_kind = Coinductive then
-	  (str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
-	else
-	  (pp_expr false env [] t)
-	in
-	(try
-	   (* First, can this match be printed as a mere record projection ? *)
-	   let fields =
-	     match info.m_kind with Record f -> f | _ -> raise Impossible
-	   in
-	   let (r, ids, c) = pv.(0) in
-	   let n = List.length ids in
-	   let free_of_patvar a = not (List.exists (ast_occurs_itvl 1 n) a) in
-	   let proj_hd i =
-	     pp_expr true env [] t ++ str "." ++ pp_field r fields i
-	   in
-	   match c with
-	     | MLrel i when i <= n -> apply (pp_par par' (proj_hd (n-i)))
-	     | MLapp (MLrel i, a) when (i <= n) && (free_of_patvar a) ->
-	       let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
-	       (pp_apply (proj_hd (n-i))
-		  par ((List.map (pp_expr true env' []) a) @ args))
-	     | _ -> raise Impossible
-	 with Impossible ->
-	   (* Second, can this match be printed as a let-in ? *)
-	   if Array.length pv = 1 then
-	     let s1,s2 = pp_one_pat env info pv.(0) in
-	     apply
-	       (hv 0
-		  (pp_par par'
-		     (hv 0
-			(hov 2 (str "let " ++ s1 ++ str " =" ++ spc () ++ expr)
-			 ++ spc () ++ str "in") ++
-		      spc () ++ hov 0 s2)))
-	   else
-	     (* Otherwise, standard match *)
- 	     apply
-      	       (pp_par par'
-		  (try pp_ifthenelse par' env expr pv
-		   with Not_found ->
-		     v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++
-			  pp_pat env info pv))))
     | MLfix (i,ids,defs) ->
 	let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
-      	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
+	pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
     | MLexn s ->
 	(* An [MLexn] may be applied, but I don't really care. *)
 	pp_par par (str "assert false" ++ spc () ++ str ("(* "^s^" *)"))
@@ -290,7 +201,96 @@ let rec pp_expr par env args =
 	pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args)
     | MLaxiom ->
 	pp_par par (str "failwith \"AXIOM TO BE REALIZED\"")
-
+    | MLcons (_,r,a) as c ->
+        assert (args=[]);
+        begin match a with
+	  | _ when is_native_char c -> pp_native_char c
+	  | [a1;a2] when is_infix r ->
+	    let pp = pp_expr true env [] in
+	    pp_par par (pp a1 ++ str (get_infix r) ++ pp a2)
+	  | _ when is_coinductive r ->
+	    let ne = (a<>[]) in
+	    let tuple = space_if ne ++ pp_tuple (pp_expr true env []) a in
+	    pp_par par (str "lazy " ++ pp_par ne (pp_global Cons r ++ tuple))
+	  | [] -> pp_global Cons r
+	  | _ ->
+	    let fds = get_record_fields r in
+	    if fds <> [] then
+	      pp_record_pat (pp_fields r fds, List.map (pp_expr true env []) a)
+	    else
+	      let tuple = pp_tuple (pp_expr true env []) a in
+	      if str_global Cons r = "" (* hack Extract Inductive prod *)
+	      then tuple
+	      else pp_par par (pp_global Cons r ++ spc () ++ tuple)
+	end
+    | MLtuple l ->
+        assert (args = []);
+        pp_boxed_tuple (pp_expr true env []) l
+    | MLcase (_, t, pv) when is_custom_match pv ->
+        if not (is_regular_match pv) then
+	  error "Cannot mix yet user-given match and general patterns.";
+	let mkfun (ids,_,e) =
+	  if ids <> [] then named_lams (List.rev ids) e
+	  else dummy_lams (ast_lift 1 e) 1
+	in
+	let pp_branch tr = pp_expr true env [] (mkfun tr) ++ fnl () in
+	let inner =
+	  str (find_custom_match pv) ++ fnl () ++
+	  prvect pp_branch pv ++
+	  pp_expr true env [] t
+	in
+	apply2 (hov 2 inner)
+    | MLcase (typ, t, pv) ->
+        let head =
+	  if not (is_coinductive_type typ) then pp_expr false env [] t
+	  else (str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
+	in
+	(* First, can this match be printed as a mere record projection ? *)
+        (try pp_record_proj par env typ t pv args
+	 with Impossible ->
+	   (* Second, can this match be printed as a let-in ? *)
+	   if Array.length pv = 1 then
+	     let s1,s2 = pp_one_pat env pv.(0) in
+	     hv 0 (apply2 (pp_letin s1 head s2))
+	   else
+	     (* Third, can this match be printed as [if ... then ... else] ? *)
+	     (try apply2 (pp_ifthenelse env head pv)
+	      with Not_found ->
+		(* Otherwise, standard match *)
+		apply2
+		  (v 0 (str "match " ++ head ++ str " with" ++ fnl () ++
+			pp_pat env pv))))
+
+and pp_record_proj par env typ t pv args =
+  (* Can a match be printed as a mere record projection ? *)
+  let fields = record_fields_of_type typ in
+  if fields = [] then raise Impossible;
+  if Array.length pv <> 1 then raise Impossible;
+  if has_deep_pattern pv then raise Impossible;
+  let (ids,pat,body) = pv.(0) in
+  let n = List.length ids in
+  let no_patvar a = not (List.exists (ast_occurs_itvl 1 n) a) in
+  let rel_i,a = match body with
+    | MLrel i when i <= n -> i,[]
+    | MLapp(MLrel i, a) when i<=n && no_patvar a -> i,a
+    | _ -> raise Impossible
+  in
+  let rec lookup_rel i idx = function
+    | Prel j :: l -> if i = j then idx else lookup_rel i (idx+1) l
+    | Pwild :: l -> lookup_rel i (idx+1) l
+    | _ -> raise Impossible
+  in
+  let r,idx = match pat with
+    | Pusual r -> r, n-rel_i
+    | Pcons (r,l) -> r, lookup_rel rel_i 0 l
+    | _ -> raise Impossible
+  in
+  if is_infix r then raise Impossible;
+  let env' = snd (push_vars (List.rev_map id_of_mlid ids) env) in
+  let pp_args = (List.map (pp_expr true env' []) a) @ args in
+  let pp_head = pp_expr true env [] t ++ str "." ++ pp_field r fields idx
+  in
+  pp_apply pp_head par pp_args
 
 and pp_record_pat (fields, args) =
    str "{ " ++
@@ -299,9 +299,27 @@ and pp_record_pat (fields, args) =
      (List.combine fields args) ++
    str " }"
 
-and pp_ifthenelse par env expr pv = match pv with
-  | [|(tru,[],the);(fal,[],els)|] when
-      (find_custom tru = "true") && (find_custom fal = "false")
+and pp_cons_pat r ppl =
+  if is_infix r && List.length ppl = 2 then
+    List.hd ppl ++ str (get_infix r) ++ List.hd (List.tl ppl)
+  else
+    let fields = get_record_fields r in
+    if fields <> [] then pp_record_pat (pp_fields r fields, ppl)
+    else if str_global Cons r = "" then
+      pp_boxed_tuple identity ppl (* Hack Extract Inductive prod *)
+    else
+      pp_global Cons r ++ space_if (ppl<>[]) ++ pp_boxed_tuple identity ppl
+
+and pp_gen_pat ids env = function
+  | Pcons (r, l) -> pp_cons_pat r (List.map (pp_gen_pat ids env) l)
+  | Pusual r -> pp_cons_pat r (List.map pr_id ids)
+  | Ptuple l -> pp_boxed_tuple (pp_gen_pat ids env) l
+  | Pwild -> str "_"
+  | Prel n -> pr_id (get_db_name n env)
+
+and pp_ifthenelse env expr pv = match pv with
+  | [|([],tru,the);([],fal,els)|] when
+      (is_bool_patt tru "true") && (is_bool_patt fal "false")
       ->
       hv 0 (hov 2 (str "if " ++ expr) ++ spc () ++
             hov 2 (str "then " ++
@@ -310,66 +328,34 @@ and pp_ifthenelse par env expr pv = match pv with
 	           hov 2 (pp_expr (expr_needs_par els) env [] els)))
   | _ -> raise Not_found
 
-and pp_one_pat env info (r,ids,t) =
-  let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
-  let expr = pp_expr (expr_needs_par t) env' [] t in
-  let patt = match info.m_kind with
-    | Record fields ->
-      pp_record_pat (pp_fields r fields, List.rev_map pr_id ids)
-    | _ -> match List.rev ids with
-	| [i1;i2] when is_infix r -> pr_id i1 ++ str (get_infix r) ++ pr_id i2
-	| [] -> pp_global Cons r
-	| ids ->
-	  (* hack Extract Inductive prod *)
-	  (if str_global Cons r = "" then mt () else pp_global Cons r ++ spc ())
-	  ++ pp_boxed_tuple pr_id ids
-  in
-  patt, expr
-
-and pp_pat env info pv =
-  let factor_br, factor_set = try match info.m_same with
-    | BranchFun ints ->
-        let i = Intset.choose ints in
-        branch_as_fun info.m_typs pv.(i), ints
-    | BranchCst ints ->
-        let i = Intset.choose ints in
-	ast_pop (branch_as_cst pv.(i)), ints
-    | BranchNone -> MLdummy, Intset.empty
-  with _ -> MLdummy, Intset.empty
-  in
-  let last = Array.length pv - 1 in
+and pp_one_pat env (ids,p,t) =
+  let ids',env' = push_vars (List.rev_map id_of_mlid ids) env in
+  pp_gen_pat (List.rev ids') env' p,
+  pp_expr (expr_needs_par t) env' [] t
+
+and pp_pat env pv =
   prvecti
-    (fun i x -> if Intset.mem i factor_set then mt () else
-       let s1,s2 = pp_one_pat env info x in
+    (fun i x ->
+       let s1,s2 = pp_one_pat env x in
        hv 2 (hov 4 (str "| " ++ s1 ++ str " ->") ++ spc () ++ hov 2 s2) ++
-       if i = last && Intset.is_empty factor_set then mt () else fnl ())
+       if i = Array.length pv - 1 then mt () else fnl ())
     pv
-  ++
-  if Intset.is_empty factor_set then mt () else
-  let par = expr_needs_par factor_br in
-  match info.m_same with
-    | BranchFun _ ->
-        let ids, env' = push_vars [anonymous_name] env in
-        hv 2 (str "| " ++ pr_id (List.hd ids) ++ str " ->" ++ spc () ++
-		 hov 2 (pp_expr par env' [] factor_br))
-    | BranchCst _ ->
-        hv 2 (str "| _ ->" ++ spc () ++ hov 2 (pp_expr par env [] factor_br))
-    | BranchNone -> mt ()
 
 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
-	i.m_kind = Standard && not (is_custom_match pv) ->
-	if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then
+    | MLcase(Tglob(r,_),MLrel 1,pv) when
+	not (is_coinductive r) && get_record_fields r = [] &&
+	not (is_custom_match pv) ->
+	if not (ast_occurs 1 (MLcase(Tunknown,MLdummy,pv))) then
 	  pr_binding (List.rev (List.tl bl)) ++
        	  str " = function" ++ fnl () ++
-	  v 0 (pp_pat env' i pv)
+	  v 0 (pp_pat env' pv)
 	else
           pr_binding (List.rev bl) ++
           str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++
-	  v 0 (pp_pat env' i pv)
+	  v 0 (pp_pat env' pv)
     | _ ->
           pr_binding (List.rev bl) ++
 	  str " =" ++ fnl () ++ str "  " ++
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 8a781a8d9..215076555 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -85,7 +85,7 @@ let rec pp_expr env args =
 		    ++ spc () ++ hov 0 (pp_expr env' [] a2)))))
     | MLglob r ->
 	apply (pp_global Term r)
-    | MLcons (info,r,args') ->
+    | MLcons (_,r,args') ->
 	assert (args=[]);
 	let st =
 	  str "`" ++
@@ -93,9 +93,12 @@ let rec pp_expr env args =
 		 (if args' = [] then mt () else spc ()) ++
 		 prlist_with_sep spc (pp_cons_args env) args')
 	in
-	if info.c_kind = Coinductive then paren (str "delay " ++ st) else st
+	if is_coinductive r then paren (str "delay " ++ st) else st
+    | MLtuple _ -> error "Cannot handle tuples in Scheme yet."
+    | MLcase (_,_,pv) when not (is_regular_match pv) ->
+	error "Cannot handle general patterns in Scheme yet."
     | MLcase (_,t,pv) when is_custom_match pv ->
-	let mkfun (_,ids,e) =
+	let mkfun (ids,_,e) =
 	  if ids <> [] then named_lams (List.rev ids) e
 	  else dummy_lams (ast_lift 1 e) 1
 	in
@@ -105,9 +108,9 @@ let rec pp_expr env args =
 		(str (find_custom_match pv) ++ fnl () ++
 		 prvect (fun tr -> pp_expr env [] (mkfun tr) ++ fnl ()) pv
 		 ++ pp_expr env [] t)))
-     | MLcase (info,t, pv) ->
-	let e =
-	  if info.m_kind <> Coinductive then pp_expr env [] t
+    | MLcase (typ,t, pv) ->
+        let e =
+	  if not (is_coinductive_type typ) then pp_expr env [] t
 	  else paren (str "force" ++ spc () ++ pp_expr env [] t)
 	in
 	apply (v 3 (paren (str "match " ++ e ++ fnl () ++ pp_pat env pv)))
@@ -124,14 +127,18 @@ let rec pp_expr env args =
     | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"")
 
 and pp_cons_args env = function
-  | MLcons (info,r,args) when info.c_kind<>Coinductive ->
+  | MLcons (_,r,args) when is_coinductive r ->
       paren (pp_global Cons r ++
 	     (if args = [] then mt () else spc ()) ++
 	     prlist_with_sep spc (pp_cons_args env) args)
   | e -> str "," ++ pp_expr env [] e
 
-
-and pp_one_pat env (r,ids,t) =
+and pp_one_pat env (ids,p,t) =
+  let r = match p with
+    | Pusual r -> r
+    | Pcons (r,l) -> r (* cf. the check [is_regular_match] above *)
+    | _ -> assert false
+  in
   let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
   let args =
     if ids = [] then mt ()
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 567b0727c..238befd25 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -127,6 +127,39 @@ let add_ind kn mib ml_ind =
   inductives := Mindmap_env.add kn (mib,ml_ind) !inductives
 let lookup_ind kn = Mindmap_env.find kn !inductives
 
+let inductive_kinds =
+  ref (Mindmap_env.empty : inductive_kind Mindmap_env.t)
+let init_inductive_kinds () = inductive_kinds := Mindmap_env.empty
+let add_inductive_kind kn k =
+    inductive_kinds := Mindmap_env.add kn k !inductive_kinds
+let is_coinductive r =
+  let kn = match r with
+    | ConstructRef ((kn,_),_) -> kn
+    | IndRef (kn,_) -> kn
+    | _ -> assert false
+  in
+  try Mindmap_env.find kn !inductive_kinds = Coinductive
+  with Not_found -> false
+
+let is_coinductive_type = function
+  | Tglob (r,_) -> is_coinductive r
+  | _ -> false
+
+let get_record_fields r =
+  let kn = match r with
+    | ConstructRef ((kn,_),_) -> kn
+    | IndRef (kn,_) -> kn
+    | _ -> assert false
+  in
+  try match Mindmap_env.find kn !inductive_kinds with
+    | Record f -> f
+    | _ -> []
+  with Not_found -> []
+
+let record_fields_of_type = function
+  | Tglob (r,_) -> get_record_fields r
+  | _ -> []
+
 (*s Recursors table. *)
 
 (* NB: here we can use the equivalence between canonical
@@ -199,15 +232,26 @@ let library () = !library_ref
 (*s Printing. *)
 
 (* The following functions work even on objects not in [Global.env ()].
-   WARNING: for inductive objects, an extract_inductive must have been
-   done before. *)
-
-let safe_basename_of_global = function
-  | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l
-  | IndRef (kn,i) -> (snd (lookup_ind kn)).ind_packets.(i).ip_typename
-  | ConstructRef ((kn,i),j) ->
-      (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1)
-  | _ -> assert false
+   Warning: for inductive objects, this only works if an [extract_inductive]
+   have been done earlier, otherwise we can only ask the Nametab about
+   currently visible objects. *)
+
+let safe_basename_of_global r =
+  let last_chance r =
+    try Nametab.basename_of_global r
+    with Not_found ->
+      anomaly "Inductive object unknown to extraction and not globally visible"
+  in
+  match r with
+    | ConstRef kn -> id_of_label (con_label kn)
+    | IndRef (kn,0) -> id_of_label (mind_label kn)
+    | IndRef (kn,i) ->
+      (try (snd (lookup_ind kn)).ind_packets.(i).ip_typename
+       with Not_found -> last_chance r)
+    | ConstructRef ((kn,i),j) ->
+      (try (snd (lookup_ind kn)).ind_packets.(i).ip_consnames.(j-1)
+       with Not_found -> last_chance r)
+    | VarRef _ -> assert false
 
 let string_of_global r =
  try string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r)
@@ -731,8 +775,10 @@ let add_custom_match r s =
 
 let indref_of_match pv =
   if Array.length pv = 0 then raise Not_found;
-  match pv.(0) with
-    | (ConstructRef (ip,_), _, _) -> IndRef ip
+  let (_,pat,_) = pv.(0) in
+  match pat with
+    | Pusual (ConstructRef (ip,_)) -> IndRef ip
+    | Pcons (ConstructRef (ip,_),_) -> IndRef ip
     | _ -> raise Not_found
 
 let is_custom_match pv =
@@ -817,5 +863,6 @@ let extract_inductive r s l optstr =
 (*s Tables synchronization. *)
 
 let reset_tables () =
-  init_terms (); init_types (); init_inductives (); init_recursors ();
+  init_terms (); init_types (); init_inductives ();
+  init_inductive_kinds (); init_recursors ();
   init_projs (); init_axioms (); init_opaques (); reset_modfile ()
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index cdd792222..a3b7124e1 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -74,6 +74,14 @@ val lookup_type : constant -> ml_schema
 val add_ind : mutual_inductive -> mutual_inductive_body -> ml_ind -> unit
 val lookup_ind : mutual_inductive -> mutual_inductive_body * ml_ind
 
+val add_inductive_kind : mutual_inductive -> inductive_kind -> unit
+val is_coinductive : global_reference -> bool
+val is_coinductive_type : ml_type -> bool
+(* What are the fields of a record (empty for a non-record) *)
+val get_record_fields :
+  global_reference -> global_reference option list
+val record_fields_of_type : ml_type -> global_reference option list
+
 val add_recursors : Environ.env -> mutual_inductive -> unit
 val is_recursor : global_reference -> bool