Imported Upstream version 8.4~betaupstream/8.4_beta

29 files changed, 1003 insertions, 768 deletions

diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v
index eab2f67c..c9556972 100644
--- a/plugins/extraction/ExtrOcamlBasic.v
+++ b/plugins/extraction/ExtrOcamlBasic.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,8 +8,6 @@
 
 (** Extraction to Ocaml : use of basic Ocaml types *)
 
-Scheme Equality for nat.
-
 Extract Inductive bool => bool [ true false ].
 Extract Inductive option => option [ Some None ].
 Extract Inductive unit => unit [ "()" ].
diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v
index e38d41e3..69e72918 100644
--- a/plugins/extraction/ExtrOcamlBigIntConv.v
+++ b/plugins/extraction/ExtrOcamlBigIntConv.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/extraction/ExtrOcamlIntConv.v b/plugins/extraction/ExtrOcamlIntConv.v
index b059b2a0..697ea6b3 100644
--- a/plugins/extraction/ExtrOcamlIntConv.v
+++ b/plugins/extraction/ExtrOcamlIntConv.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v
index 1fb83c5b..0a303b63 100644
--- a/plugins/extraction/ExtrOcamlNatBigInt.v
+++ b/plugins/extraction/ExtrOcamlNatBigInt.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (** Extraction of [nat] into Ocaml's [big_int] *)
 
-Require Import Arith Even Div2 EqNat MinMax Euclid.
+Require Import Arith Even Div2 EqNat Euclid.
 Require Import ExtrOcamlBasic.
 
 (** NB: The extracted code should be linked with [nums.cm(x)a]
@@ -36,7 +36,7 @@ Extract Constant pred => "fun n -> Big.max Big.zero (Big.pred n)".
 Extract Constant minus => "fun n m -> Big.max Big.zero (Big.sub n m)".
 Extract Constant max => "Big.max".
 Extract Constant min => "Big.min".
-Extract Constant nat_beq => "Big.eq".
+(*Extract Constant nat_beq => "Big.eq".*)
 Extract Constant EqNat.beq_nat => "Big.eq".
 Extract Constant EqNat.eq_nat_decide => "Big.eq".
 
diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v
index e577ebe1..a0cb26b5 100644
--- a/plugins/extraction/ExtrOcamlNatInt.v
+++ b/plugins/extraction/ExtrOcamlNatInt.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (** Extraction of [nat] into Ocaml's [int] *)
 
-Require Import Arith Even Div2 EqNat MinMax Euclid.
+Require Import Arith Even Div2 EqNat Euclid.
 Require Import ExtrOcamlBasic.
 
 (** Disclaimer: trying to obtain efficient certified programs
@@ -45,7 +45,7 @@ Extract Constant minus => "fun n m -> max 0 (n-m)".
 Extract Constant mult => "( * )".
 Extract Inlined Constant max => max.
 Extract Inlined Constant min => min.
-Extract Inlined Constant nat_beq => "(=)".
+(*Extract Inlined Constant nat_beq => "(=)".*)
 Extract Inlined Constant EqNat.beq_nat => "(=)".
 Extract Inlined Constant EqNat.eq_nat_decide => "(=)".
 
@@ -72,4 +72,4 @@ Definition test n m (H:m>0) :=
  nat_compare n (q*m+r).
 
 Recursive Extraction test fact.
-*)
\ No newline at end of file
+*)
diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v
index 48260e3d..f8f942c8 100644
--- a/plugins/extraction/ExtrOcamlString.v
+++ b/plugins/extraction/ExtrOcamlString.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v
index 5ca6bd7b..12607b3a 100644
--- a/plugins/extraction/ExtrOcamlZBigInt.v
+++ b/plugins/extraction/ExtrOcamlZBigInt.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (** Extraction of [positive], [N] and [Z] into Ocaml's [big_int] *)
 
-Require Import ZArith NArith ZOdiv_def.
+Require Import ZArith NArith.
 Require Import ExtrOcamlBasic.
 
 (** NB: The extracted code should be linked with [nums.cm(x)a]
@@ -36,42 +36,44 @@ Extract Inductive N => "Big.big_int"
 
 (** Efficient (but uncertified) versions for usual functions *)
 
-Extract Constant Pplus => "Big.add".
-Extract Constant Psucc => "Big.succ".
-Extract Constant Ppred => "fun n -> Big.max Big.one (Big.pred n)".
-Extract Constant Pminus => "fun n m -> Big.max Big.one (Big.sub n m)".
-Extract Constant Pmult => "Big.mult".
-Extract Constant Pmin => "Big.min".
-Extract Constant Pmax => "Big.max".
-Extract Constant Pcompare =>
+Extract Constant Pos.add => "Big.add".
+Extract Constant Pos.succ => "Big.succ".
+Extract Constant Pos.pred => "fun n -> Big.max Big.one (Big.pred n)".
+Extract Constant Pos.sub => "fun n m -> Big.max Big.one (Big.sub n m)".
+Extract Constant Pos.mul => "Big.mult".
+Extract Constant Pos.min => "Big.min".
+Extract Constant Pos.max => "Big.max".
+Extract Constant Pos.compare =>
+ "fun x y -> Big.compare_case Eq Lt Gt x y".
+Extract Constant Pos.compare_cont =>
  "fun x y c -> Big.compare_case c Lt Gt x y".
 
-Extract Constant Nplus => "Big.add".
-Extract Constant Nsucc => "Big.succ".
-Extract Constant Npred => "fun n -> Big.max Big.zero (Big.pred n)".
-Extract Constant Nminus => "fun n m -> Big.max Big.zero (Big.sub n m)".
-Extract Constant Nmult => "Big.mult".
-Extract Constant Nmin => "Big.min".
-Extract Constant Nmax => "Big.max".
-Extract Constant Ndiv =>
+Extract Constant N.add => "Big.add".
+Extract Constant N.succ => "Big.succ".
+Extract Constant N.pred => "fun n -> Big.max Big.zero (Big.pred n)".
+Extract Constant N.sub => "fun n m -> Big.max Big.zero (Big.sub n m)".
+Extract Constant N.mul => "Big.mult".
+Extract Constant N.min => "Big.min".
+Extract Constant N.max => "Big.max".
+Extract Constant N.div =>
  "fun a b -> if Big.eq b Big.zero then Big.zero else Big.div a b".
-Extract Constant Nmod =>
+Extract Constant N.modulo =>
  "fun a b -> if Big.eq b Big.zero then Big.zero else Big.modulo a b".
-Extract Constant Ncompare => "Big.compare_case Eq Lt Gt".
-
-Extract Constant Zplus => "Big.add".
-Extract Constant Zsucc => "Big.succ".
-Extract Constant Zpred => "Big.pred".
-Extract Constant Zminus => "Big.sub".
-Extract Constant Zmult => "Big.mult".
-Extract Constant Zopp => "Big.opp".
-Extract Constant Zabs => "Big.abs".
-Extract Constant Zmin => "Big.min".
-Extract Constant Zmax => "Big.max".
-Extract Constant Zcompare => "Big.compare_case Eq Lt Gt".
-
-Extract Constant Z_of_N => "fun p -> p".
-Extract Constant Zabs_N => "Big.abs".
+Extract Constant N.compare => "Big.compare_case Eq Lt Gt".
+
+Extract Constant Z.add => "Big.add".
+Extract Constant Z.succ => "Big.succ".
+Extract Constant Z.pred => "Big.pred".
+Extract Constant Z.sub => "Big.sub".
+Extract Constant Z.mul => "Big.mult".
+Extract Constant Z.opp => "Big.opp".
+Extract Constant Z.abs => "Big.abs".
+Extract Constant Z.min => "Big.min".
+Extract Constant Z.max => "Big.max".
+Extract Constant Z.compare => "Big.compare_case Eq Lt Gt".
+
+Extract Constant Z.of_N => "fun p -> p".
+Extract Constant Z.abs_N => "Big.abs".
 
 (** Zdiv and Zmod are quite complex to define in terms of (/) and (mod).
     For the moment we don't even try *)
diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v
index a7046626..55ba0ca1 100644
--- a/plugins/extraction/ExtrOcamlZInt.v
+++ b/plugins/extraction/ExtrOcamlZInt.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,7 +8,7 @@
 
 (** Extraction of [positive], [N] and [Z] into Ocaml's [int] *)
 
-Require Import ZArith NArith ZOdiv_def.
+Require Import ZArith NArith.
 Require Import ExtrOcamlBasic.
 
 (** Disclaimer: trying to obtain efficient certified programs
@@ -33,44 +33,46 @@ Extract Inductive N => int [ "0" "" ]
 
 (** Efficient (but uncertified) versions for usual functions *)
 
-Extract Constant Pplus => "(+)".
-Extract Constant Psucc => "succ".
-Extract Constant Ppred => "fun n -> max 1 (n-1)".
-Extract Constant Pminus => "fun n m -> max 1 (n-m)".
-Extract Constant Pmult => "( * )".
-Extract Constant Pmin => "min".
-Extract Constant Pmax => "max".
-Extract Constant Pcompare =>
+Extract Constant Pos.add => "(+)".
+Extract Constant Pos.succ => "succ".
+Extract Constant Pos.pred => "fun n -> max 1 (n-1)".
+Extract Constant Pos.sub => "fun n m -> max 1 (n-m)".
+Extract Constant Pos.mul => "( * )".
+Extract Constant Pos.min => "min".
+Extract Constant Pos.max => "max".
+Extract Constant Pos.compare =>
+ "fun x y -> if x=y then Eq else if x<y then Lt else Gt".
+Extract Constant Pos.compare_cont =>
  "fun x y c -> if x=y then c else if x<y then Lt else Gt".
 
 
-Extract Constant Nplus => "(+)".
-Extract Constant Nsucc => "succ".
-Extract Constant Npred => "fun n -> max 0 (n-1)".
-Extract Constant Nminus => "fun n m -> max 0 (n-m)".
-Extract Constant Nmult => "( * )".
-Extract Constant Nmin => "min".
-Extract Constant Nmax => "max".
-Extract Constant Ndiv => "fun a b -> if b=0 then 0 else a/b".
-Extract Constant Nmod => "fun a b -> if b=0 then a else a mod b".
-Extract Constant Ncompare =>
+Extract Constant N.add => "(+)".
+Extract Constant N.succ => "succ".
+Extract Constant N.pred => "fun n -> max 0 (n-1)".
+Extract Constant N.sub => "fun n m -> max 0 (n-m)".
+Extract Constant N.mul => "( * )".
+Extract Constant N.min => "min".
+Extract Constant N.max => "max".
+Extract Constant N.div => "fun a b -> if b=0 then 0 else a/b".
+Extract Constant N.modulo => "fun a b -> if b=0 then a else a mod b".
+Extract Constant N.compare =>
  "fun x y -> if x=y then Eq else if x<y then Lt else Gt".
 
 
-Extract Constant Zplus => "(+)".
-Extract Constant Zsucc => "succ".
-Extract Constant Zpred => "pred".
-Extract Constant Zminus => "(-)".
-Extract Constant Zmult => "( * )".
-Extract Constant Zopp => "(~-)".
-Extract Constant Zabs => "abs".
-Extract Constant Zmin => "min".
-Extract Constant Zmax => "max".
-Extract Constant Zcompare =>
+Extract Constant Z.add => "(+)".
+Extract Constant Z.succ => "succ".
+Extract Constant Z.pred => "pred".
+Extract Constant Z.sub => "(-)".
+Extract Constant Z.mul => "( * )".
+Extract Constant Z.opp => "(~-)".
+Extract Constant Z.abs => "abs".
+Extract Constant Z.min => "min".
+Extract Constant Z.max => "max".
+Extract Constant Z.compare =>
  "fun x y -> if x=y then Eq else if x<y then Lt else Gt".
 
-Extract Constant Z_of_N => "fun p -> p".
-Extract Constant Zabs_N => "abs".
+Extract Constant Z.of_N => "fun p -> p".
+Extract Constant Z.abs_N => "abs".
 
 (** Zdiv and Zmod are quite complex to define in terms of (/) and (mod).
     For the moment we don't even try *)
diff --git a/plugins/extraction/big.ml b/plugins/extraction/big.ml
index ae04ba6d..4c33691d 100644
--- a/plugins/extraction/big.ml
+++ b/plugins/extraction/big.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 9713fcd2..0bd5b843 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: common.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Pp
 open Util
 open Names
@@ -35,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 ()
@@ -54,8 +76,6 @@ let fnl2 () = fnl () ++ fnl ()
 
 let space_if = function true -> str " " | false -> mt ()
 
-let sec_space_if = function true -> spc () | false -> mt ()
-
 let is_digit = function
   | '0'..'9' -> true
   | _ -> false
@@ -352,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 22bad6cd..02a496be 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: common.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Names
 open Libnames
 open Miniml
@@ -22,10 +20,19 @@ open Pp
 val fnl : unit -> std_ppcmds
 val fnl2 : unit -> std_ppcmds
 val space_if : bool -> std_ppcmds
-val sec_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.ml b/plugins/extraction/extract_env.ml
index 3fa674d3..73062328 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extract_env.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Term
 open Declarations
 open Names
@@ -40,21 +38,19 @@ let toplevel_env () =
 	in l,seb
     | _ -> failwith "caught"
   in
-  match current_toplevel () with
-    | _ -> SEBstruct (List.rev (map_succeed get_reference seg))
- 
+  SEBstruct (List.rev (map_succeed get_reference seg))
+
 
 let environment_until dir_opt =
   let rec parse = function
     | [] when dir_opt = None -> [current_toplevel (), toplevel_env ()]
     | [] -> []
     | d :: l ->
-      let mb = Global.lookup_module (MPfile d) in
-      (* If -dont-load-proof has been used, mod_expr is None,
-         we try with mod_type *)
-      let meb = Option.default mb.mod_type mb.mod_expr in
-      if dir_opt = Some d then [MPfile d, meb]
-      else (MPfile d, meb) :: (parse l)
+	match (Global.lookup_module (MPfile d)).mod_expr with
+	  | Some meb ->
+	      if dir_opt = Some d then [MPfile d, meb]
+	      else (MPfile d, meb) :: (parse l)
+	  | _ -> assert false
   in parse (Library.loaded_libraries ())
 
 
@@ -68,6 +64,9 @@ module type VISIT = sig
   (* Add the module_path and all its prefixes to the mp visit list *)
   val add_mp : module_path -> unit
 
+  (* Same, but we'll keep all fields of these modules *)
+  val add_mp_all : module_path -> unit
+
   (* Add kernel_name / constant / reference / ... in the visit lists.
      These functions silently add the mp of their arg in the mp list *)
   val add_ind : mutual_inductive -> unit
@@ -81,6 +80,7 @@ module type VISIT = sig
   val needed_ind : mutual_inductive -> bool
   val needed_con : constant -> bool
   val needed_mp : module_path -> bool
+  val needed_mp_all : module_path -> bool
 end
 
 module Visit : VISIT = struct
@@ -88,16 +88,26 @@ module Visit : VISIT = struct
      (for inductives and modules names) and a Cset_env for constants
      (and still the remaining MPset) *)
   type must_visit =
-      { mutable ind : KNset.t; mutable con : KNset.t; mutable mp : MPset.t }
+      { mutable ind : KNset.t; mutable con : KNset.t;
+	mutable mp : MPset.t; mutable mp_all : MPset.t }
   (* the imperative internal visit lists *)
-  let v = { ind = KNset.empty ; con = KNset.empty ; mp = MPset.empty }
+  let v = { ind = KNset.empty ; con = KNset.empty ;
+	    mp = MPset.empty; mp_all = MPset.empty }
   (* the accessor functions *)
-  let reset () = v.ind <- KNset.empty; v.con <- KNset.empty; v.mp <- MPset.empty
+  let reset () =
+    v.ind <- KNset.empty;
+    v.con <- KNset.empty;
+    v.mp <- MPset.empty;
+    v.mp_all <- MPset.empty
   let needed_ind i = KNset.mem (user_mind i) v.ind
   let needed_con c = KNset.mem (user_con c) v.con
-  let needed_mp mp = MPset.mem mp v.mp
+  let needed_mp mp = MPset.mem mp v.mp || MPset.mem mp v.mp_all
+  let needed_mp_all mp = MPset.mem mp v.mp_all
   let add_mp mp =
     check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp
+  let add_mp_all mp =
+    check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp;
+    v.mp_all <- MPset.add mp v.mp_all
   let add_ind i =
     let kn = user_mind i in
     v.ind <- KNset.add kn v.ind; add_mp (modpath kn)
@@ -120,12 +130,17 @@ let check_arity env cb =
 
 let check_fix env cb i =
   match cb.const_body with
-    | None -> raise Impossible
-    | Some lbody ->
-	match kind_of_term (Declarations.force lbody) with
+    | Def lbody ->
+	(match kind_of_term (Declarations.force lbody) with
 	  | Fix ((_,j),recd) when i=j -> check_arity env cb; (true,recd)
 	  | CoFix (j,recd) when i=j -> check_arity env cb; (false,recd)
-	  | _ -> raise Impossible
+	  | _ -> raise Impossible)
+    | Undef _ | OpaqueDef _ -> raise Impossible
+
+let prec_declaration_equal (na1, ca1, ta1) (na2, ca2, ta2) =
+  na1 = na2 &&
+  array_equal eq_constr ca1 ca2 &&
+  array_equal eq_constr ta1 ta2
 
 let factor_fix env l cb msb =
   let _,recd as check = check_fix env cb 0 in
@@ -139,7 +154,8 @@ let factor_fix env l cb msb =
       (fun j ->
 	 function
 	   | (l,SFBconst cb') ->
-	       if check <> check_fix env cb' (j+1) then raise Impossible;
+	       let check' = check_fix env cb' (j+1) in
+	       if not (fst check = fst check' && prec_declaration_equal (snd check) (snd check')) then raise Impossible;
 	       labels.(j+1) <- l;
 	   | _ -> raise Impossible) msb';
     labels, recd, msb''
@@ -157,7 +173,8 @@ let rec seb2mse = function
 
 let expand_seb env mp seb =
   let seb,_,_,_ =
-    Mod_typing.translate_struct_module_entry env mp true (seb2mse seb)
+    let inl = Some (Flags.get_inline_level()) in
+    Mod_typing.translate_struct_module_entry env mp inl (seb2mse seb)
   in seb
 
 (** When possible, we use the nicer, shorter, algebraic type structures
@@ -200,9 +217,8 @@ let rec extract_sfb_spec env mp = function
       if logical_spec s then specs
       else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
   | (l,SFBmind _) :: msig ->
-      let kn = make_kn mp empty_dirpath l in
-      let mind = mind_of_kn kn in
-      let s = Sind (kn, extract_inductive env mind) in
+      let mind = make_mind mp empty_dirpath l in
+      let s = Sind (mind, extract_inductive env mind) in
       let specs = extract_sfb_spec env mp msig in
       if logical_spec s then specs
       else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
@@ -223,7 +239,7 @@ let rec extract_sfb_spec env mp = function
 *)
 
 and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with
-  | SEBident mp -> Visit.add_mp mp; MTident mp
+  | SEBident mp -> Visit.add_mp_all mp; MTident mp
   | SEBwith(seb',With_definition_body(idl,cb))->
       let env' = env_for_mtb_with env (msid_of_seb seb') seb idl in
       let mt = extract_seb_spec env mp1 (seb,seb') in
@@ -231,7 +247,7 @@ and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with
 	 | None -> mt
 	 | Some (vl,typ) -> MTwith(mt,ML_With_type(idl,vl,typ)))
   | SEBwith(seb',With_module_body(idl,mp))->
-      Visit.add_mp mp;
+      Visit.add_mp_all mp;
       MTwith(extract_seb_spec env mp1 (seb,seb'),
 	     ML_With_module(idl,mp))
   | SEBfunctor (mbid, mtb, seb_alg') ->
@@ -283,11 +299,10 @@ let rec extract_sfb env mp all = function
 	 else ms)
   | (l,SFBmind mib) :: msb ->
       let ms = extract_sfb env mp all msb in
-      let kn = make_kn mp empty_dirpath l in
-      let mind = mind_of_kn kn in
+      let mind = make_mind mp empty_dirpath l in
       let b = Visit.needed_ind mind in
       if all || b then
-	let d = Dind (kn, extract_inductive env mind) in
+	let d = Dind (mind, extract_inductive env mind) in
 	if (not b) && (logical_decl d) then ms
 	else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
       else ms
@@ -312,7 +327,7 @@ and extract_seb env mp all = function
       extract_seb env mp all (expand_seb env mp seb)
   | SEBident mp ->
       if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false;
-      Visit.add_mp mp; MEident mp
+      Visit.add_mp_all mp; MEident mp
   | SEBapply (meb, meb',_) ->
       MEapply (extract_seb env mp true meb,
 	       extract_seb env mp true meb')
@@ -346,11 +361,12 @@ let unpack = function MEstruct (_,sel) -> sel | _ -> assert false
 let mono_environment refs mpl =
   Visit.reset ();
   List.iter Visit.add_ref refs;
-  List.iter Visit.add_mp mpl;
+  List.iter Visit.add_mp_all mpl;
   let env = Global.env () in
   let l = List.rev (environment_until None) in
   List.rev_map
-    (fun (mp,m) -> mp, unpack (extract_seb env mp false m)) l
+    (fun (mp,m) -> mp, unpack (extract_seb env mp (Visit.needed_mp_all mp) m))
+    l
 
 (**************************************)
 (*S Part II : Input/Output primitives *)
@@ -488,13 +504,18 @@ let print_structure_to_file (fn,si,mo) dry struc =
 let reset () =
   Visit.reset (); reset_tables (); reset_renaming_tables Everything
 
-let init modular =
+let init modular library =
   check_inside_section (); check_inside_module ();
   set_keywords (descr ()).keywords;
   set_modular modular;
+  set_library library;
   reset ();
   if modular && lang () = Scheme then error_scheme ()
 
+let warns () =
+  warning_opaques (access_opaque ());
+  warning_axioms ()
+
 (* From a list of [reference], let's retrieve whether they correspond
    to modules or [global_reference]. Warn the user if both is possible. *)
 
@@ -503,7 +524,8 @@ let rec locate_ref = function
   | r::l ->
       let q = snd (qualid_of_reference r) in
       let mpo = try Some (Nametab.locate_module q) with Not_found -> None
-      and ro = try Some (Nametab.locate q) with Not_found -> None in
+      and ro = try Some (Smartlocate.global_with_alias r) with _ -> None
+      in
       match mpo, ro with
 	| None, None -> Nametab.error_global_not_found q
 	| None, Some r -> let refs,mps = locate_ref l in r::refs,mps
@@ -518,25 +540,41 @@ let rec locate_ref = function
     \verb!Extraction "file"! [qualid1] ... [qualidn]. *)
 
 let full_extr f (refs,mps) =
-  init false;
+  init false false;
   List.iter (fun mp -> if is_modfile mp then error_MPfile_as_mod mp true) mps;
-  let struc = optimize_struct refs (mono_environment refs mps) in
-  warning_axioms ();
+  let struc = optimize_struct (refs,mps) (mono_environment refs mps) in
+  warns ();
   print_structure_to_file (mono_filename f) false struc;
   reset ()
 
 let full_extraction f lr = full_extr f (locate_ref lr)
 
+(*s Separate extraction is similar to recursive extraction, with the output
+   decomposed in many files, one per Coq .v file *)
+
+let separate_extraction lr =
+  init true false;
+  let refs,mps = locate_ref lr in
+  let struc = optimize_struct (refs,mps) (mono_environment refs mps) in
+  warns ();
+  let print = function
+    | (MPfile dir as mp, sel) as e ->
+	print_structure_to_file (module_filename mp) false [e]
+    | _ -> assert false
+  in
+  List.iter print struc;
+  reset ()
+
 (*s Simple extraction in the Coq toplevel. The vernacular command
     is \verb!Extraction! [qualid]. *)
 
 let simple_extraction r = match locate_ref [r] with
   | ([], [mp]) as p -> full_extr None p
   | [r],[] ->
-      init false;
-      let struc = optimize_struct [r] (mono_environment [r] []) in
+      init false false;
+      let struc = optimize_struct ([r],[]) (mono_environment [r] []) in
       let d = get_decl_in_structure r struc in
-      warning_axioms ();
+      warns ();
       if is_custom r then msgnl (str "(** User defined extraction *)");
       print_one_decl struc (modpath_of_r r) d;
       reset ()
@@ -547,12 +585,12 @@ let simple_extraction r = match locate_ref [r] with
   \verb!(Recursive) Extraction Library! [M]. *)
 
 let extraction_library is_rec m =
-  init true;
+  init true true;
   let dir_m =
     let q = qualid_of_ident m in
     try Nametab.full_name_module q with Not_found -> error_unknown_module q
   in
-  Visit.add_mp (MPfile dir_m);
+  Visit.add_mp_all (MPfile dir_m);
   let env = Global.env () in
   let l = List.rev (environment_until (Some dir_m)) in
   let select l (mp,meb) =
@@ -561,8 +599,8 @@ let extraction_library is_rec m =
     else l
   in
   let struc = List.fold_left select [] l in
-  let struc = optimize_struct [] struc in
-  warning_axioms ();
+  let struc = optimize_struct ([],[]) struc in
+  warns ();
   let print = function
     | (MPfile dir as mp, sel) as e ->
 	let dry = not is_rec && dir <> dir_m in
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 145cd6b3..e587bf21 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extract_env.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (*s This module declares the extraction commands. *)
 
 open Names
@@ -15,9 +13,15 @@ open Libnames
 
 val simple_extraction : reference -> unit
 val full_extraction : string option -> reference list -> unit
+val separate_extraction : reference list -> unit
 val extraction_library : bool -> identifier -> unit
 
 (* For debug / external output via coqtop.byte + Drop : *)
 
 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 27f32a4a..219b3913 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extraction.ml 14786 2011-12-10 12:55:19Z letouzey $ i*)
-
 (*i*)
 open Util
 open Names
@@ -48,8 +46,6 @@ let sort_of env c =
     Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c)
   with SingletonInductiveBecomesProp id -> error_singleton_become_prop id
 
-let is_axiom env kn = (Environ.lookup_constant kn env).const_body = None
-
 (*S Generation of flags and signatures. *)
 
 (* The type [flag] gives us information about any Coq term:
@@ -197,6 +193,27 @@ let parse_ind_args si args relmax =
 	 | _ -> parse (i+1) (j+1) s)
   in parse 1 1 si
 
+let oib_equal o1 o2 =
+  id_ord o1.mind_typename o2.mind_typename = 0 &&
+  list_equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt &&
+  begin match o1.mind_arity, o2.mind_arity with
+  | Monomorphic {mind_user_arity=c1; mind_sort=s1},
+    Monomorphic {mind_user_arity=c2; mind_sort=s2} ->
+      eq_constr c1 c2 && s1 = s2
+  | ma1, ma2 -> ma1 = ma2 end &&
+  o1.mind_consnames = o2.mind_consnames
+
+let mib_equal m1 m2 =
+  array_equal oib_equal m1.mind_packets m1.mind_packets &&
+  m1.mind_record = m2.mind_record &&
+  m1.mind_finite = m2.mind_finite &&
+  m1.mind_ntypes = m2.mind_ntypes &&
+  list_equal eq_named_declaration m1.mind_hyps m2.mind_hyps &&
+  m1.mind_nparams = m2.mind_nparams &&
+  m1.mind_nparams_rec = m2.mind_nparams_rec &&
+  list_equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt &&
+  m1.mind_constraints = m2.mind_constraints
+
 (*S Extraction of a type. *)
 
 (* [extract_type env db c args] is used to produce an ML type from the
@@ -215,7 +232,7 @@ let rec extract_type env db j c args =
 	extract_type env db j d (Array.to_list args' @ args)
     | Lambda (_,_,d) ->
 	(match args with
-	   | [] -> assert false (* otherwise the lambda would be reductible. *)
+	   | [] -> assert false (* A lambda cannot be a type. *)
 	   | a :: args -> extract_type env db j (subst1 a d) args)
     | Prod (n,t,d) ->
 	assert (args = []);
@@ -255,12 +272,13 @@ let rec extract_type env db j c args =
 	let cb = lookup_constant kn env in
 	let typ = Typeops.type_of_constant_type env cb.const_type in
 	(match flag_of_type env typ with
+	   | (Logic,_) -> assert false (* Cf. logical cases above *)
 	   | (Info, TypeScheme) ->
 	       let mlt = extract_type_app env db (r, type_sign env typ) args in
 	       (match cb.const_body with
-		  | None -> mlt
-		  | Some _ when is_custom r -> mlt
-		  | Some lbody ->
+		  | Undef _ | OpaqueDef _ -> mlt
+		  | Def _ when is_custom r -> mlt
+		  | Def lbody ->
 		      let newc = applist (Declarations.force lbody, args) in
 		      let mlt' = extract_type env db j newc [] in
 		      (* ML type abbreviations interact badly with Coq *)
@@ -269,10 +287,11 @@ let rec extract_type env db j c args =
 		      (* The shortest is [mlt], which use abbreviations *)
 		      (* If possible, we take [mlt], otherwise [mlt']. *)
 		      if expand env mlt = expand env mlt' then mlt else mlt')
-	   | _ -> (* only other case here: Info, Default, i.e. not an ML type *)
+	   | (Info, Default) ->
+               (* Not an ML type, for example [(c:forall X, X->X) Type nat] *)
 	       (match cb.const_body with
-		  | None -> Tunknown (* Brutal approximation ... *)
-		  | Some lbody ->
+		  | Undef _  | OpaqueDef _ -> Tunknown (* Brutal approx ... *)
+		  | Def lbody ->
 		      (* We try to reduce. *)
 		      let newc = applist (Declarations.force lbody, args) in
 		      extract_type env db j newc []))
@@ -282,14 +301,6 @@ let rec extract_type env db j c args =
     | Case _ | Fix _ | CoFix _ -> Tunknown
     | _ -> assert false
 
-(* [extract_maybe_type] calls [extract_type] when used on a Coq type,
-   and otherwise returns [Tdummy] or [Tunknown] *)
-
-and extract_maybe_type env db c =
-  let t = whd_betadeltaiota env none (type_of env c) in
-  if isSort t then extract_type env db 0 c []
-  else if sort_of env t = InProp then Tdummy Kother else Tunknown
-
 (*s Auxiliary function dealing with type application.
   Precondition: [r] is a type scheme represented by the signature [s],
   and is completely applied: [List.length args = List.length s]. *)
@@ -337,13 +348,18 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
        We hence check that the mib has not changed from recording
        time to retrieving time. Ideally we should also check the env. *)
     let (mib0,ml_ind) = lookup_ind kn in
-    if not (mib = mib0) then raise Not_found;
+    if not (mib_equal mib mib0) then raise Not_found;
     ml_ind
   with Not_found ->
-    (* First, if this inductive is aliased via a Module, *)
-    (* we process the original inductive. *)
-    let equiv = 
-      if (canonical_mind kn) = (user_mind kn) then
+    (* First, if this inductive is aliased via a Module,
+       we process the original inductive if possible.
+       When at toplevel of the monolithic case, we cannot do much
+       (cf Vector and bug #2570) *)
+    let equiv =
+      if lang () <> Ocaml ||
+	 (not (modular ()) && at_toplevel (mind_modpath kn)) ||
+	 kn_ord (canonical_mind kn) (user_mind kn) = 0
+      then
 	NoEquiv
       else
 	begin
@@ -370,8 +386,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	     ip_logical = (not b);
 	     ip_sign = s;
 	     ip_vars = v;
-	     ip_types = t;
-	     ip_optim_id_ok = None })
+	     ip_types = t })
 	mib.mind_packets
     in
 
@@ -412,7 +427,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);
@@ -464,6 +480,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
@@ -496,8 +513,8 @@ and mlt_env env r = match r with
 	 let cb = Environ.lookup_constant kn env in
 	 let typ = Typeops.type_of_constant_type env cb.const_type in
 	 match cb.const_body with
-	   | None -> None
-	   | Some l_body ->
+	   | Undef _ | OpaqueDef _ -> None
+	   | Def l_body ->
 	       (match flag_of_type env typ with
 		  | Info,TypeScheme ->
 		      let body = Declarations.force l_body in
@@ -560,6 +577,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;
@@ -727,8 +746,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
@@ -792,22 +811,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. *)
 
@@ -869,7 +888,7 @@ let extract_std_constant env kn body typ =
     and m = nb_lam body in
     if n <= m then decompose_lam_n n body
     else
-      let s,s' = list_split_at m s in
+      let s,s' = list_chop m s in
       if List.for_all ((=) Keep) s' &&
 	(lang () = Haskell || sign_kind s <> UnsafeLogicalSig)
       then decompose_lam_n m body
@@ -878,7 +897,7 @@ let extract_std_constant env kn body typ =
   (* Should we do one eta-expansion to avoid non-generalizable '_a ? *)
   let rels, c =
     let n = List.length rels in
-    let s,s' = list_split_at n s in
+    let s,s' = list_chop n s in
     let k = sign_kind s in
     let empty_s = (k = EmptySig || k = SafeLogicalSig) in
     if lang () = Ocaml && empty_s && not (gentypvar_ok c)
@@ -888,7 +907,7 @@ let extract_std_constant env kn body typ =
   in
   let n = List.length rels in
   let s = list_firstn n s in
-  let l,l' = list_split_at n l in
+  let l,l' = list_chop n l in
   let t' = type_recomp (l',t') in
   (* The initial ML environment. *)
   let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in
@@ -925,34 +944,45 @@ let extract_fixpoint env vkn (fi,ti,ci) =
 let extract_constant env kn cb =
   let r = ConstRef kn in
   let typ = Typeops.type_of_constant_type env cb.const_type in
-  match cb.const_body with
-    | None -> (* A logical axiom is risky, an informative one is fatal. *)
-        (match flag_of_type env typ with
-	   | (Info,TypeScheme) ->
-	       if not (is_custom r) then add_info_axiom r;
-	       let n = type_scheme_nb_args env typ in
-	       let ids = iterate (fun l -> anonymous_name::l) n [] in
-	       Dtype (r, ids, Taxiom)
-           | (Info,Default) ->
-	       if not (is_custom r) then add_info_axiom r;
-	       let t = snd (record_constant_type env kn (Some typ)) in
-	       Dterm (r, MLaxiom, type_expunge env t)
-           | (Logic,TypeScheme) ->
-	       add_log_axiom r; Dtype (r, [], Tdummy Ktype)
-	   | (Logic,Default) ->
-	       add_log_axiom r; Dterm (r, MLdummy, Tdummy Kother))
-    | Some body ->
-	(match flag_of_type env typ with
-	   | (Logic, Default) -> Dterm (r, MLdummy, Tdummy Kother)
-	   | (Logic, TypeScheme) -> Dtype (r, [], Tdummy Ktype)
-	   | (Info, Default) ->
-	       let e,t = extract_std_constant env kn (force body) typ in
-	       Dterm (r,e,t)
-	   | (Info, TypeScheme) ->
-	       let s,vl = type_sign_vl env typ in
-               let db = db_from_sign s in
-               let t = extract_type_scheme env db (force body) (List.length s)
-	       in Dtype (r, vl, t))
+  let warn_info () = if not (is_custom r) then add_info_axiom r in
+  let warn_log () = if not (constant_has_body cb) then add_log_axiom r
+  in
+  let mk_typ_ax () =
+    let n = type_scheme_nb_args env typ in
+    let ids = iterate (fun l -> anonymous_name::l) n [] in
+    Dtype (r, ids, Taxiom)
+  in
+  let mk_typ c =
+    let s,vl = type_sign_vl env typ in
+    let db = db_from_sign s in
+    let t = extract_type_scheme env db c (List.length s)
+    in Dtype (r, vl, t)
+  in
+  let mk_ax () =
+    let t = snd (record_constant_type env kn (Some typ)) in
+    Dterm (r, MLaxiom, type_expunge env t)
+  in
+  let mk_def c =
+    let e,t = extract_std_constant env kn c typ in
+    Dterm (r,e,t)
+  in
+  match flag_of_type env typ with
+    | (Logic,TypeScheme) -> warn_log (); Dtype (r, [], Tdummy Ktype)
+    | (Logic,Default) -> warn_log (); Dterm (r, MLdummy, Tdummy Kother)
+    | (Info,TypeScheme) ->
+        (match cb.const_body with
+	  | Undef _ -> warn_info (); mk_typ_ax ()
+	  | Def c -> mk_typ (force c)
+	  | OpaqueDef c ->
+	    add_opaque r;
+	    if access_opaque () then mk_typ (force_opaque c) else mk_typ_ax ())
+    | (Info,Default) ->
+        (match cb.const_body with
+	  | Undef _ -> warn_info (); mk_ax ()
+	  | Def c -> mk_def (force c)
+	  | OpaqueDef c ->
+	    add_opaque r;
+	    if access_opaque () then mk_def (force_opaque c) else mk_ax ())
 
 let extract_constant_spec env kn cb =
   let r = ConstRef kn in
@@ -963,8 +993,8 @@ let extract_constant_spec env kn cb =
     | (Info, TypeScheme) ->
 	let s,vl = type_sign_vl env typ in
 	(match cb.const_body with
-	  | None -> Stype (r, vl, None)
-	  | Some body ->
+	  | Undef _ | OpaqueDef _ -> Stype (r, vl, None)
+	  | Def body ->
 	      let db = db_from_sign s in
 	      let t = extract_type_scheme env db (force body) (List.length s)
 	      in Stype (r, vl, Some t))
@@ -977,9 +1007,13 @@ let extract_with_type env cb =
   match flag_of_type env typ with
     | (Info, TypeScheme) ->
 	let s,vl = type_sign_vl env typ in
-	let body = Option.get cb.const_body in
 	let db = db_from_sign s in
-	let t = extract_type_scheme env db (force body) (List.length s) in
+	let c = match cb.const_body with
+	  | Def body -> force body
+	  (* A "with Definition ..." is necessarily transparent *)
+	  | Undef _ | OpaqueDef _ -> assert false
+	in
+	let t = extract_type_scheme env db c (List.length s) in
 	Some (vl, t)
     | _ -> None
 
@@ -995,7 +1029,7 @@ let extract_inductive env kn =
 	  let l' = filter (succ i) l in
 	  if isDummy (expand env t) || List.mem i implicits then l'
 	  else t::l'
-    in filter 1 l
+    in filter (1+ind.ind_nparams) l
   in
   let packets =
     Array.mapi (fun i p -> { p with ip_types = Array.mapi (f i) p.ip_types })
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index 8a2125fe..48f05acb 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: extraction.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (*s Extraction from Coq terms to Miniml. *)
 
 open Names
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index ebd4de0d..11a2d0e0 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -63,6 +63,12 @@ VERNAC COMMAND EXTEND Extraction
   -> [ full_extraction (Some f) l ]
 END
 
+VERNAC COMMAND EXTEND SeparateExtraction
+(* Same, with content splitted in several files *)
+| [ "Separate" "Extraction" ne_global_list(l) ]
+  -> [ separate_extraction l ]
+END
+
 (* Modular extraction (one Coq library = one ML module) *)
 VERNAC COMMAND EXTEND ExtractionLibrary
 | [ "Extraction" "Library" ident(m) ]
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index aeacef93..96731ed2 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: haskell.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (*s Production of Haskell syntax. *)
 
 open Pp
@@ -47,15 +45,15 @@ let preamble mod_name used_modules usf =
   (if used_modules = [] then mt () else fnl ()) ++
   (if not usf.magic then mt ()
    else str "\
-unsafeCoerce :: a -> b
-#ifdef __GLASGOW_HASKELL__
-import qualified GHC.Base
-unsafeCoerce = GHC.Base.unsafeCoerce#
-#else
--- HUGS
-import qualified IOExts
-unsafeCoerce = IOExts.unsafeCoerce
-#endif" ++ fnl2 ())
+\nunsafeCoerce :: a -> b\
+\n#ifdef __GLASGOW_HASKELL__\
+\nimport qualified GHC.Base\
+\nunsafeCoerce = GHC.Base.unsafeCoerce#\
+\n#else\
+\n-- HUGS\
+\nimport qualified IOExts\
+\nunsafeCoerce = IOExts.unsafeCoerce\
+\n#endif" ++ fnl2 ())
   ++
   (if not usf.mldummy then mt ()
    else str "__ :: any" ++ fnl () ++
@@ -78,17 +76,17 @@ let pp_global k r =
 
 let kn_sig =
   let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in
-  make_kn specif empty_dirpath (mk_label "sig")
+  make_mind specif empty_dirpath (mk_label "sig")
 
 let rec pp_type par vl t =
   let rec pp_rec par = function
     | Tmeta _ | Tvar' _ -> assert false
     | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i))
     | Tglob (r,[]) -> pp_global Type r
-    | Tglob (r,l) ->
-	if r = IndRef (mind_of_kn kn_sig,0) then
+    | Tglob (IndRef(kn,0),l)
+	when not (keep_singleton ()) && kn = mk_ind "Coq.Init.Specif" "sig" ->
 	  pp_type true vl (List.hd l)
-	else
+    | Tglob (r,l) ->
 	  pp_par par
 	    (pp_global Type r ++ spc () ++
 	     prlist_with_sep spc (pp_type true vl) l)
@@ -113,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)
@@ -125,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)
@@ -135,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
@@ -178,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. *)
@@ -293,12 +283,10 @@ let rec pp_ind first kn i ind =
 
 (*s Pretty-printing of a declaration. *)
 
-let pp_string_parameters ids = prlist (fun id -> str id ++ str " ")
-
 let pp_decl = function
   | Dind (kn,i) when i.ind_kind = Singleton ->
-      pp_singleton (mind_of_kn kn) i.ind_packets.(0) ++ fnl ()
-  | Dind (kn,i) -> hov 0 (pp_ind true (mind_of_kn kn) 0 i)
+      pp_singleton kn i.ind_packets.(0) ++ fnl ()
+  | Dind (kn,i) -> hov 0 (pp_ind true kn 0 i)
   | Dtype (r, l, t) ->
       if is_inline_custom r then mt ()
       else
diff --git a/plugins/extraction/haskell.mli b/plugins/extraction/haskell.mli
index eb774db7..0f8949e3 100644
--- a/plugins/extraction/haskell.mli
+++ b/plugins/extraction/haskell.mli
@@ -1,12 +1,10 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: haskell.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 val haskell_descr : Miniml.language_descr
 
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index aaf2d0c3..5a19cc3f 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: miniml.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (*s Target language for extraction: a core ML called MiniML. *)
 
 open Pp
@@ -73,8 +71,7 @@ type ml_ind_packet = {
   ip_logical : bool;
   ip_sign : signature;
   ip_vars : identifier list;
-  ip_types : (ml_type list) array;
-  mutable ip_optim_id_ok : bool option
+  ip_types : (ml_type list) array
 }
 
 (* [ip_nparams] contains the number of parameters. *)
@@ -99,28 +96,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
@@ -128,24 +114,32 @@ 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 =
-  | Dind  of kernel_name * ml_ind
+  | Dind  of mutual_inductive * ml_ind
   | Dtype of global_reference * identifier list * ml_type
   | Dterm of global_reference * ml_ast * ml_type
   | Dfix  of global_reference array * ml_ast array * ml_type array
 
 type ml_spec =
-  | Sind  of kernel_name * ml_ind
+  | Sind  of mutual_inductive * ml_ind
   | Stype of global_reference * identifier list * ml_type option
   | Sval  of global_reference * ml_type
 
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 3c7ee0f2..c244e046 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: mlutil.ml 14786 2011-12-10 12:55:19Z letouzey $ i*)
-
 (*i*)
 open Pp
 open Util
@@ -56,18 +54,6 @@ let new_meta _ =
   incr meta_count;
   Tmeta {id = !meta_count; contents = None}
 
-(*s Sustitution of [Tvar i] by [t] in a ML type. *)
-
-let type_subst i t0 t =
-  let rec subst t = match t with
-    | Tvar j when i = j -> t0
-    | Tmeta {contents=None} -> t
-    | Tmeta {contents=Some u} -> subst u
-    | Tarr (a,b) -> Tarr (subst a, subst b)
-    | Tglob (r, l) -> Tglob (r, List.map subst l)
-    | a -> a
-  in subst t
-
 (* Simultaneous substitution of [[Tvar 1; ... ; Tvar n]] by [l] in a ML type. *)
 
 let type_subst_list l t =
@@ -378,54 +364,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  -> ()
 
@@ -446,15 +439,6 @@ let ast_occurs_itvl k k' t =
     ast_iter_rel (fun i -> if (k <= i) && (i <= k') then raise Found) t; false
   with Found -> true
 
-(*s Number of occurences of [Rel k] (resp. [Rel 1]) in [t]. *)
-
-let nb_occur_k k t =
-  let cpt = ref 0 in
-  ast_iter_rel (fun i -> if i = k then incr cpt) t;
-  !cpt
-
-let nb_occur t = nb_occur_k 1 t
-
 (* Number of occurences of [Rel 1] in [t], with special treatment of match:
    occurences in different branches aren't added, but we rather use max. *)
 
@@ -464,13 +448,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
@@ -530,6 +514,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
@@ -577,7 +594,6 @@ let rec many_lams id a = function
   | 0 -> a
   | n -> many_lams id (MLlam (id,a)) (pred n)
 
-let anonym_lams a n = many_lams anonymous a n
 let anonym_tmp_lams a n = many_lams (Tmp anonymous_name) a n
 let dummy_lams a n = many_lams Dummy a n
 
@@ -679,26 +695,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]).
@@ -706,7 +727,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
@@ -745,20 +766,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. *)
 
@@ -781,14 +809,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)
@@ -796,32 +824,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
@@ -853,9 +892,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
@@ -891,40 +930,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]. *)
@@ -1149,28 +1198,24 @@ 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
 
-let rec is_constr = function
-  | MLcons _   -> true
-  | MLlam(_,t) -> is_constr t
-  | _          -> false
-
 (*s Strictness *)
 
 (* A variable is strict if the evaluation of the whole term implies
@@ -1219,7 +1264,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
@@ -1265,12 +1310,14 @@ let inline_test r t =
   if not (auto_inline ()) then false
   else
     let c = match r with ConstRef c -> c | _ -> assert false in
-    let body = try (Global.lookup_constant c).const_body with _ -> None in
-    if body = None then false
-    else
-      let t1 = eta_red t in
-      let t2 = snd (collect_lams t1) in
-      not (is_fix t2) && ml_size t < 12 && is_not_strict t
+    let has_body =
+      try constant_has_body (Global.lookup_constant c)
+      with _ -> false
+    in
+    has_body &&
+      (let t1 = eta_red t in
+       let t2 = snd (collect_lams t1) in
+       not (is_fix t2) && ml_size t < 12 && is_not_strict t)
 
 let con_of_string s =
   let null = empty_dirpath in
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 54a1baaa..029e8cf4 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: mlutil.mli 14786 2011-12-10 12:55:19Z letouzey $ i*)
-
 open Util
 open Names
 open Term
@@ -20,7 +18,6 @@ open Table
 val reset_meta_count : unit -> unit
 val new_meta : 'a -> ml_type
 
-val type_subst : int -> ml_type -> ml_type -> ml_type
 val type_subst_list : ml_type list -> ml_type -> ml_type
 val type_subst_vect : ml_type array -> ml_type -> ml_type
 
@@ -118,9 +115,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 ffa38def..9e8dd828 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modutil.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Names
 open Declarations
 open Environ
@@ -28,7 +26,7 @@ let rec msid_of_mt = function
 (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a
    [ml_structure]. *)
 
-let struct_iter do_decl do_spec s =
+let se_iter do_decl do_spec =
   let rec mt_iter = function
     | MTident _ -> ()
     | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt'
@@ -58,7 +56,10 @@ let struct_iter do_decl do_spec s =
     | MEapply (me,me') -> me_iter me; me_iter me'
     | MEstruct (msid, sel) -> List.iter se_iter sel
   in
-  List.iter (function (_,sel) -> List.iter se_iter sel) s
+  se_iter
+
+let struct_iter do_decl do_spec s =
+  List.iter (function (_,sel) -> List.iter (se_iter do_decl do_spec) sel) s
 
 (*s Apply some fonctions upon all references in [ml_type], [ml_ast],
   [ml_decl], [ml_spec] and [ml_structure]. *)
@@ -76,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 =
@@ -108,15 +117,14 @@ let decl_iter_references do_term do_cons do_type =
   let type_iter = type_iter_references do_type
   and ast_iter = ast_iter_references do_term do_cons do_type in
   function
-    | Dind (kn,ind) -> ind_iter_references do_term do_cons do_type 
-	(mind_of_kn kn) ind
+    | Dind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind
     | Dtype (r,_,t) -> do_type r; type_iter t
     | Dterm (r,a,t) -> do_term r; ast_iter a; type_iter t
     | Dfix(rv,c,t) ->
 	Array.iter do_term rv; Array.iter ast_iter c; Array.iter type_iter t
 
 let spec_iter_references do_term do_cons do_type = function
-  | Sind (kn,ind) -> ind_iter_references do_term do_cons do_type (mind_of_kn kn) ind
+  | Sind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind
   | Stype (r,_,ot) -> do_type r; Option.iter (type_iter_references do_type) ot
   | Sval (r,t) -> do_term r; type_iter_references do_type t
 
@@ -236,7 +244,7 @@ let rec optim_se top to_appear s = function
       let a = normalize (ast_glob_subst !s a) in
       let i = inline r a in
       if i then s := Refmap'.add r a !s;
-      if top && i && not (modular ()) && not (List.mem r to_appear)
+      if top && i && not (library ()) && not (List.mem r to_appear)
       then optim_se top to_appear s lse
       else
 	let d = match optimize_fix a with
@@ -254,7 +262,7 @@ let rec optim_se top to_appear s = function
 	then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s
 	else all := false
       done;
-      if !all && top && not (modular ())
+      if !all && top && not (library ())
 	&& (array_for_all (fun r -> not (List.mem r to_appear)) rv)
       then optim_se top to_appear s lse
       else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse)
@@ -271,7 +279,8 @@ and optim_me to_appear s = function
   | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me to_appear s me)
 
 (* After these optimisations, some dependencies may not be needed anymore.
-   For monolithic extraction, we recompute a minimal set of dependencies. *)
+   For non-library extraction, we recompute a minimal set of dependencies
+   for first-level objects *)
 
 exception NoDepCheck
 
@@ -281,15 +290,19 @@ let base_r = function
   | ConstructRef ((kn,_),_) -> IndRef (kn,0)
   | _ -> assert false
 
-let reset_needed, add_needed, found_needed, is_needed =
-  let needed = ref Refset'.empty in
-  ((fun l -> needed := Refset'.empty),
+let reset_needed, add_needed, add_needed_mp, found_needed, is_needed =
+  let needed = ref Refset'.empty
+  and needed_mps = ref MPset.empty in
+  ((fun l -> needed := Refset'.empty; needed_mps := MPset.empty),
    (fun r -> needed := Refset'.add (base_r r) !needed),
+   (fun mp -> needed_mps := MPset.add mp !needed_mps),
    (fun r -> needed := Refset'.remove (base_r r) !needed),
-   (fun r -> Refset'.mem (base_r r) !needed))
+   (fun r ->
+     let r = base_r r in
+     Refset'.mem r !needed || MPset.mem (modpath_of_r r) !needed_mps))
 
 let declared_refs = function
-  | Dind (kn,_) -> [IndRef (mind_of_kn kn,0)]
+  | Dind (kn,_) -> [IndRef (kn,0)]
   | Dtype (r,_,_) -> [r]
   | Dterm (r,_,_) -> [r]
   | Dfix (rv,_,_) -> Array.to_list rv
@@ -300,7 +313,7 @@ let declared_refs = function
 let compute_deps_decl = function
   | Dind (kn,ind) ->
       (* Todo Later : avoid dependencies when Extract Inductive *)
-      ind_iter_references add_needed add_needed add_needed (mind_of_kn kn) ind
+      ind_iter_references add_needed add_needed add_needed kn ind
   | Dtype (r,ids,t) ->
       if not (is_custom r) then type_iter_references add_needed t
   | Dterm (r,u,t) ->
@@ -310,6 +323,15 @@ let compute_deps_decl = function
   | Dfix _ as d ->
       decl_iter_references add_needed add_needed add_needed d
 
+let compute_deps_spec = function
+  | Sind (kn,ind) ->
+      (* Todo Later : avoid dependencies when Extract Inductive *)
+      ind_iter_references add_needed add_needed add_needed kn ind
+  | Stype (r,ids,t) ->
+      if not (is_custom r) then Option.iter (type_iter_references add_needed) t
+  | Sval (r,t) ->
+      type_iter_references add_needed t
+
 let rec depcheck_se = function
   | [] -> []
   | ((l,SEdecl d) as t) :: se ->
@@ -317,7 +339,9 @@ let rec depcheck_se = function
     let refs = declared_refs d in
     let refs' = List.filter is_needed refs in
     if refs' = [] then
-      (List.iter remove_info_axiom refs; se')
+      (List.iter remove_info_axiom refs;
+       List.iter remove_opaque refs;
+       se')
     else begin
       List.iter found_needed refs';
       (* Hack to avoid extracting unused part of a Dfix *)
@@ -327,7 +351,10 @@ let rec depcheck_se = function
 	  ((l,SEdecl (Dfix (rv,trms',tys))) :: se')
 	| _ -> (compute_deps_decl d; t::se')
     end
-  | _ -> raise NoDepCheck
+  | t :: se ->
+    let se' = depcheck_se se in
+    se_iter compute_deps_decl compute_deps_spec t;
+    t :: se'
 
 let rec depcheck_struct = function
   | [] -> []
@@ -350,13 +377,15 @@ let check_implicits = function
 let optimize_struct to_appear struc =
   let subst = ref (Refmap'.empty : ml_ast Refmap'.t) in
   let opt_struc =
-    List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc
+    List.map (fun (mp,lse) -> (mp, optim_se true (fst to_appear) subst lse))
+      struc
   in
   let opt_struc = List.filter (fun (_,lse) -> lse<>[]) opt_struc in
   ignore (struct_ast_search check_implicits opt_struc);
-  try
-    if modular () then raise NoDepCheck;
+  if library () then opt_struc
+  else begin
     reset_needed ();
-    List.iter add_needed to_appear;
+    List.iter add_needed (fst to_appear);
+    List.iter add_needed_mp (snd to_appear);
     depcheck_struct opt_struc
-  with NoDepCheck -> opt_struc
+  end
diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli
index 26d07872..0565522b 100644
--- a/plugins/extraction/modutil.mli
+++ b/plugins/extraction/modutil.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modutil.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Names
 open Declarations
 open Environ
@@ -38,4 +36,5 @@ val get_decl_in_structure : global_reference -> ml_structure -> ml_decl
    optimizations. The first argument is the list of objects we want to appear.
 *)
 
-val optimize_struct : global_reference list -> ml_structure -> ml_structure
+val optimize_struct : global_reference list * module_path list ->
+  ml_structure -> ml_structure
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index c07a1758..ed69ec45 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ocaml.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (*s Production of Ocaml syntax. *)
 
 open Pp
@@ -31,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  ->
@@ -59,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 =
@@ -137,7 +123,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
@@ -154,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
@@ -167,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)
@@ -179,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^" *)"))
@@ -291,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 "{ " ++
@@ -300,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 " ++
@@ -311,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 "  " ++
@@ -451,7 +436,7 @@ let pp_logical_ind packet =
   fnl ()
 
 let pp_singleton kn packet =
-  let name = pp_global Type (IndRef (mind_of_kn kn,0)) in
+  let name = pp_global Type (IndRef (kn,0)) in
   let l = rename_tvars keywords packet.ip_vars in
   hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++
 	 pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++
@@ -459,7 +444,7 @@ let pp_singleton kn packet =
 		     pr_id packet.ip_consnames.(0)))
 
 let pp_record kn fields ip_equiv packet =
-  let ind = IndRef (mind_of_kn kn,0) in
+  let ind = IndRef (kn,0) in
   let name = pp_global Type ind in
   let fieldnames = pp_fields ind fields in
   let l = List.combine fieldnames packet.ip_types.(0) in
@@ -482,20 +467,20 @@ let pp_ind co kn ind =
   let init= ref (str "type ") in
   let names =
     Array.mapi (fun i p -> if p.ip_logical then mt () else
-		  pp_global Type (IndRef (mind_of_kn kn,i)))
+		  pp_global Type (IndRef (kn,i)))
       ind.ind_packets
   in
   let cnames =
     Array.mapi
       (fun i p -> if p.ip_logical then [||] else
-	 Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((mind_of_kn kn,i),j+1)))
+	 Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((kn,i),j+1)))
 	   p.ip_types)
       ind.ind_packets
   in
   let rec pp i =
     if i >= Array.length ind.ind_packets then mt ()
     else
-      let ip = (mind_of_kn kn,i) in
+      let ip = (kn,i) in
       let ip_equiv = ind.ind_equiv, i in
       let p = ind.ind_packets.(i) in
       if is_custom (IndRef ip) then pp (i+1)
diff --git a/plugins/extraction/ocaml.mli b/plugins/extraction/ocaml.mli
index c0b4e5b3..fd60c69d 100644
--- a/plugins/extraction/ocaml.mli
+++ b/plugins/extraction/ocaml.mli
@@ -1,12 +1,10 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ocaml.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 val ocaml_descr : Miniml.language_descr
 
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 1f04ca59..21507655 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: scheme.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (*s Production of Scheme syntax. *)
 
 open Pp
@@ -87,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 "`" ++
@@ -95,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
@@ -107,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)))
@@ -126,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/scheme.mli b/plugins/extraction/scheme.mli
index c7c3d8b5..eeca083c 100644
--- a/plugins/extraction/scheme.mli
+++ b/plugins/extraction/scheme.mli
@@ -1,11 +1,9 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: scheme.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 val scheme_descr : Miniml.language_descr
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 67cf2210..238befd2 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: table.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Names
 open Term
 open Declarations
@@ -21,23 +19,11 @@ open Util
 open Pp
 open Miniml
 
-(** Sets and maps for [global_reference] that work modulo equivalent
-    on the user part of the name (otherwise use Refset / Refmap ) *)
-
-module RefOrd = struct
-  type t = global_reference
-  let compare x y =
-    let make_name = function
-      | ConstRef con -> ConstRef(constant_of_kn(user_con con))
-      | IndRef (kn,i) -> IndRef(mind_of_kn(user_mind kn),i)
-      | ConstructRef ((kn,i),j)-> ConstructRef((mind_of_kn(user_mind kn),i),j)
-      | VarRef id -> VarRef id
-    in
-    Pervasives.compare (make_name x) (make_name y)
-end
+(** Sets and maps for [global_reference] that use the "user" [kernel_name]
+    instead of the canonical one *)
 
-module Refmap' = Map.Make(RefOrd)
-module Refset' = Set.Make(RefOrd)
+module Refmap' = Map.Make(RefOrdered_env)
+module Refset' = Set.Make(RefOrdered_env)
 
 (*S Utilities about [module_path] and [kernel_names] and [global_reference] *)
 
@@ -71,11 +57,6 @@ let raw_string_of_modfile = function
   | MPfile f -> String.capitalize (string_of_id (List.hd (repr_dirpath f)))
   | _ -> assert false
 
-let rec modfile_of_mp = function
-  | (MPfile _) as mp -> mp
-  | MPdot (mp,_) -> modfile_of_mp mp
-  | _ -> raise Not_found
-
 let current_toplevel () = fst (Lib.current_prefix ())
 
 let is_toplevel mp =
@@ -109,12 +90,6 @@ let common_prefix_from_list mp0 mpl =
     | mp :: l -> if MPset.mem mp prefixes then Some mp else f l
   in f mpl
 
-let rec parse_labels ll = function
-  | MPdot (mp,l) -> parse_labels (l::ll) mp
-  | mp -> mp,ll
-
-let labels_of_mp mp = parse_labels [] mp
-
 let rec parse_labels2 ll mp1 = function
   | mp when mp1=mp -> mp,ll
   | MPdot (mp,l) -> parse_labels2 (l::ll) mp1 mp
@@ -125,10 +100,6 @@ let labels_of_ref r =
   let mp,_,l = repr_of_r r in
   parse_labels2 [l] mp_top mp
 
-let rec add_labels_mp mp = function
-  | [] -> mp
-  | l :: ll -> add_labels_mp (MPdot (mp,l)) ll
-
 
 (*S The main tables: constants, inductives, records, ... *)
 
@@ -156,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
@@ -203,25 +207,51 @@ let add_info_axiom r = info_axioms := Refset'.add r !info_axioms
 let remove_info_axiom r = info_axioms := Refset'.remove r !info_axioms
 let add_log_axiom r = log_axioms := Refset'.add r !log_axioms
 
-(*s Extraction mode: modular or monolithic *)
+let opaques = ref Refset'.empty
+let init_opaques () = opaques := Refset'.empty
+let add_opaque r = opaques := Refset'.add r !opaques
+let remove_opaque r = opaques := Refset'.remove r !opaques
+
+(*s Extraction modes: modular or monolithic, library or minimal ?
+
+Nota:
+ - Recursive Extraction : monolithic, minimal
+ - Separate Extraction : modular, minimal
+ - Extraction Library : modular, library
+*)
 
 let modular_ref = ref false
+let library_ref = ref false
 
 let set_modular b = modular_ref := b
 let modular () = !modular_ref
 
+let set_library b = library_ref := b
+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)
@@ -272,7 +302,28 @@ let warning_axioms () =
        str "Having invalid logical axiom in the environment when extracting" ++
        spc () ++ str "may lead to incorrect or non-terminating ML terms." ++
        fnl ())
-  end
+  end;
+  if !Flags.load_proofs = Flags.Dont && info_axioms@log_axioms <> [] then
+    msg_warning
+      (str "Some of these axioms might be due to option -dont-load-proofs.")
+
+let warning_opaques accessed =
+  let opaques = Refset'.elements !opaques in
+  if opaques = [] then ()
+  else
+    let lst = hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques) in
+    if accessed then
+      msg_warning
+	(str "The extraction is currently set to bypass opacity,\n" ++
+	 str "the following opaque constant bodies have been accessed :" ++
+	 lst ++ str "." ++ fnl ())
+    else
+      msg_warning
+	(str "The extraction now honors the opacity constraints by default,\n" ++
+	 str "the following opaque constants have been extracted as axioms :" ++
+	 lst ++ str "." ++ fnl () ++
+	 str "If necessary, use \"Set Extraction AccessOpaque\" to change this."
+	 ++ fnl ())
 
 let warning_both_mod_and_cst q mp r =
  msg_warning
@@ -386,31 +437,34 @@ let info_file f =
 (* The objects defined below should survive an arbitrary time,
    so we register them to coq save/undo mechanism. *)
 
-(*s Extraction AutoInline *)
+let my_bool_option name initval =
+  let flag = ref initval in
+  let access = fun () -> !flag in
+  let _ = declare_bool_option
+    {optsync = true;
+     optdepr = false;
+     optname = "Extraction "^name;
+     optkey = ["Extraction"; name];
+     optread = access;
+     optwrite = (:=) flag }
+  in
+  access
 
-let auto_inline_ref = ref false
+(*s Extraction AccessOpaque *)
 
-let auto_inline () = !auto_inline_ref
+let access_opaque = my_bool_option "AccessOpaque" false
 
-let _ = declare_bool_option
-	  {optsync = true;
-	   optname = "Extraction AutoInline";
-	   optkey = ["Extraction"; "AutoInline"];
-	   optread = auto_inline;
-	   optwrite = (:=) auto_inline_ref}
+(*s Extraction AutoInline *)
+
+let auto_inline = my_bool_option "AutoInline" false
 
 (*s Extraction TypeExpand *)
 
-let type_expand_ref = ref true
+let type_expand = my_bool_option "TypeExpand" true
 
-let type_expand () = !type_expand_ref
+(*s Extraction KeepSingleton *)
 
-let _ = declare_bool_option
-	  {optsync = true;
-	   optname = "Extraction TypeExpand";
-	   optkey = ["Extraction"; "TypeExpand"];
-	   optread = type_expand;
-	   optwrite = (:=) type_expand_ref}
+let keep_singleton = my_bool_option "KeepSingleton" false
 
 (*s Extraction Optimize *)
 
@@ -461,6 +515,7 @@ let optims () = !opt_flag_ref
 
 let _ = declare_bool_option
 	  {optsync = true;
+           optdepr = false;
 	   optname = "Extraction Optimize";
 	   optkey = ["Extraction"; "Optimize"];
 	   optread = (fun () -> !int_flag_ref <> 0);
@@ -468,6 +523,7 @@ let _ = declare_bool_option
 
 let _ = declare_int_option
           { optsync = true;
+            optdepr = false;
             optname = "Extraction Flag";
             optkey = ["Extraction";"Flag"];
             optread = (fun _ -> Some !int_flag_ref);
@@ -484,7 +540,7 @@ let lang_ref = ref Ocaml
 
 let lang () = !lang_ref
 
-let (extr_lang,_) =
+let extr_lang : lang -> obj =
   declare_object
     {(default_object "Extraction Lang") with
        cache_function = (fun (_,l) -> lang_ref := l);
@@ -516,12 +572,14 @@ let add_inline_entries b l =
 
 (* Registration of operations for rollback. *)
 
-let (inline_extraction,_) =
+let inline_extraction : bool * global_reference list -> obj =
   declare_object
     {(default_object "Extraction Inline") with
        cache_function = (fun (_,(b,l)) -> add_inline_entries b l);
        load_function = (fun _ (_,(b,l)) -> add_inline_entries b l);
        classify_function = (fun o -> Substitute o);
+       discharge_function =
+	(fun (_,(b,l)) -> Some (b, List.map pop_global_reference l));
        subst_function =
         (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
     }
@@ -534,8 +592,7 @@ let _ = declare_summary "Extraction Inline"
 (* Grammar entries. *)
 
 let extraction_inline b l =
-  check_inside_section ();
-  let refs = List.map Nametab.global l in
+  let refs = List.map Smartlocate.global_with_alias l in
   List.iter
     (fun r -> match r with
        | ConstRef _ -> ()
@@ -559,7 +616,7 @@ let print_extraction_inline () =
 
 (* Reset part *)
 
-let (reset_inline,_) =
+let reset_inline : unit -> obj =
   declare_object
     {(default_object "Reset Extraction Inline") with
        cache_function = (fun (_,_)-> inline_table :=  empty_inline_table);
@@ -598,7 +655,7 @@ let add_implicits r l =
 
 (* Registration of operations for rollback. *)
 
-let (implicit_extraction,_) =
+let implicit_extraction : global_reference * int_or_id list -> obj =
   declare_object
     {(default_object "Extraction Implicit") with
        cache_function = (fun (_,(r,l)) -> add_implicits r l);
@@ -616,7 +673,7 @@ let _ = declare_summary "Extraction Implicit"
 
 let extraction_implicit r l =
   check_inside_section ();
-  Lib.add_anonymous_leaf (implicit_extraction (Nametab.global r,l))
+  Lib.add_anonymous_leaf (implicit_extraction (Smartlocate.global_with_alias r,l))
 
 
 (*s Extraction Blacklist of filenames not to use while extracting *)
@@ -658,12 +715,11 @@ let add_blacklist_entries l =
 
 (* Registration of operations for rollback. *)
 
-let (blacklist_extraction,_) =
+let blacklist_extraction : string list -> obj =
   declare_object
     {(default_object "Extraction Blacklist") with
        cache_function = (fun (_,l) -> add_blacklist_entries l);
        load_function = (fun _ (_,l) -> add_blacklist_entries l);
-       classify_function = (fun o -> Libobject.Keep o);
        subst_function = (fun (_,x) -> x)
     }
 
@@ -686,7 +742,7 @@ let print_extraction_blacklist () =
 
 (* Reset part *)
 
-let (reset_blacklist,_) =
+let reset_blacklist : unit -> obj =
   declare_object
     {(default_object "Reset Extraction Blacklist") with
        cache_function = (fun (_,_)-> blacklist_table := Idset.empty);
@@ -719,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 =
@@ -732,7 +790,7 @@ let find_custom_match pv =
 
 (* Registration of operations for rollback. *)
 
-let (in_customs,_) =
+let in_customs : global_reference * string list * string -> obj =
   declare_object
     {(default_object "ML extractions") with
        cache_function = (fun (_,(r,ids,s)) -> add_custom r ids s);
@@ -747,7 +805,7 @@ let _ = declare_summary "ML extractions"
 	    unfreeze_function = ((:=) customs);
 	    init_function = (fun () -> customs := Refmap'.empty) }
 
-let (in_custom_matchs,_) =
+let in_custom_matchs : global_reference * string -> obj =
   declare_object
     {(default_object "ML extractions custom matchs") with
        cache_function = (fun (_,(r,s)) -> add_custom_match r s);
@@ -765,7 +823,7 @@ let _ = declare_summary "ML extractions custom match"
 
 let extract_constant_inline inline r ids s =
   check_inside_section ();
-  let g = Nametab.global r in
+  let g = Smartlocate.global_with_alias r in
   match g with
     | ConstRef kn ->
 	let env = Global.env () in
@@ -783,7 +841,7 @@ let extract_constant_inline inline r ids s =
 
 let extract_inductive r s l optstr =
   check_inside_section ();
-  let g = Nametab.global r in
+  let g = Smartlocate.global_with_alias r in
   match g with
     | IndRef ((kn,i) as ip) ->
 	let mib = Global.lookup_mind kn in
@@ -805,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_projs (); init_axioms (); reset_modfile ()
+  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 b70d3efa..a3b7124e 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: table.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 open Names
 open Libnames
 open Miniml
@@ -21,6 +19,7 @@ val safe_basename_of_global : global_reference -> identifier
 (*s Warning and Error messages. *)
 
 val warning_axioms : unit -> unit
+val warning_opaques : bool -> unit
 val warning_both_mod_and_cst :
  qualid -> module_path -> global_reference -> unit
 val warning_id : string -> unit
@@ -59,10 +58,8 @@ val at_toplevel : module_path -> bool
 val visible_con : constant -> bool
 val mp_length : module_path -> int
 val prefixes_mp : module_path -> MPset.t
-val modfile_of_mp : module_path -> module_path
 val common_prefix_from_list :
   module_path -> module_path list -> module_path option
-val add_labels_mp : module_path -> label list -> module_path
 val get_nth_label_mp : int -> module_path -> label
 val labels_of_ref : global_reference -> module_path * label list
 
@@ -77,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
 
@@ -88,8 +93,15 @@ val add_info_axiom : global_reference -> unit
 val remove_info_axiom : global_reference -> unit
 val add_log_axiom : global_reference -> unit
 
+val add_opaque : global_reference -> unit
+val remove_opaque : global_reference -> unit
+
 val reset_tables : unit -> unit
 
+(*s AccessOpaque parameter *)
+
+val access_opaque : unit -> bool
+
 (*s AutoInline parameter *)
 
 val auto_inline : unit -> bool
@@ -98,6 +110,10 @@ val auto_inline : unit -> bool
 
 val type_expand : unit -> bool
 
+(*s KeepSingleton parameter *)
+
+val keep_singleton : unit -> bool
+
 (*s Optimize parameter *)
 
 type opt_flag =
@@ -120,11 +136,20 @@ val optims :  unit -> opt_flag
 type lang = Ocaml | Haskell | Scheme
 val lang : unit -> lang
 
-(*s Extraction mode: modular or monolithic *)
+(*s Extraction modes: modular or monolithic, library or minimal ?
+
+Nota:
+ - Recursive Extraction : monolithic, minimal
+ - Separate Extraction : modular, minimal
+ - Extraction Library : modular, library
+*)
 
 val set_modular : bool -> unit
 val modular : unit -> bool
 
+val set_library : bool -> unit
+val library : unit -> bool
+
 (*s Table for custom inlining *)
 
 val to_inline : global_reference -> bool
@@ -158,6 +183,7 @@ val extract_constant_inline :
 val extract_inductive :
   reference -> string -> string list -> string option -> unit
 
+
 type int_or_id = ArgInt of int | ArgId of identifier
 val extraction_implicit : reference -> int_or_id list -> unit