Imported Upstream version 8.5~beta1+dfsg

30 files changed, 1110 insertions, 882 deletions

diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v
index 3a06c0a3..9dbda821 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-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v
index 78544d44..4cc76d86 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-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -10,7 +10,7 @@
 
 (** NB: The extracted code should be linked with [nums.cm(x)a]
     from ocaml's stdlib and with the wrapper [big.ml] that
-    simlifies the use of [Big_int] (it could be found in the sources
+    simplifies the use of [Big_int] (it can be found in the sources
     of Coq). *)
 
 Require Import Arith ZArith.
@@ -105,4 +105,4 @@ Definition check :=
 Extraction "/tmp/test.ml" check test.
 
 ... and we check that test=check
-*)
\ No newline at end of file
+*)
diff --git a/plugins/extraction/ExtrOcamlIntConv.v b/plugins/extraction/ExtrOcamlIntConv.v
index 424a42c5..eb43d69f 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-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \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 926b8c6c..1386c2ad 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-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -13,7 +13,7 @@ Require Import ExtrOcamlBasic.
 
 (** NB: The extracted code should be linked with [nums.cm(x)a]
     from ocaml's stdlib and with the wrapper [big.ml] that
-    simlifies the use of [Big_int] (it could be found in the sources
+    simplifies the use of [Big_int] (it can be found in the sources
     of Coq). *)
 
 (** Disclaimer: trying to obtain efficient certified programs
diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v
index 105298e0..5f653ee1 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-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v
index aee3c386..ce8025bf 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-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \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 6e98a377..3d59669a 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-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -13,7 +13,7 @@ Require Import ExtrOcamlBasic.
 
 (** NB: The extracted code should be linked with [nums.cm(x)a]
     from ocaml's stdlib and with the wrapper [big.ml] that
-    simlifies the use of [Big_int] (it could be found in the sources
+    simplifies the use of [Big_int] (it can be found in the sources
     of Coq). *)
 
 (** Disclaimer: trying to obtain efficient certified programs
diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v
index ea001c80..79d67495 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-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -43,7 +43,7 @@ Extract Constant Pos.max => "Pervasives.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".
+ "fun c x y -> if x=y then c else if x<y then Lt else Gt".
 
 
 Extract Constant N.add => "(+)".
diff --git a/plugins/extraction/README b/plugins/extraction/README
index 64c871fd..458ba0de 100644
--- a/plugins/extraction/README
+++ b/plugins/extraction/README
@@ -6,7 +6,7 @@
 What is it ?
 ------------
 
-The extraction is a mechanism allowing to produce functional code
+The extraction is a mechanism that produces functional code
 (Ocaml/Haskell/Scheme) out of any Coq terms (either programs or
 proofs).
 
@@ -14,7 +14,7 @@ Who did it ?
 ------------
 
 The current implementation (from version 7.0 up to now) has been done
-by P. Letouzey during his PhD, helped by J.C. Filliâtre and supervised
+by P. Letouzey during his PhD, helped by J.C. Filliâtre and supervised
 by C. Paulin. 
 
 An earlier implementation (versions 6.x) was due to B. Werner and
@@ -118,7 +118,7 @@ Axioms, and then "Extract Constant ..."
 
 
 [1]:
-Exécution de termes de preuves: une nouvelle méthode d'extraction 
+Exécution de termes de preuves: une nouvelle méthode d'extraction 
 pour le Calcul des Constructions Inductives, Pierre Letouzey,
 DEA thesis, 2000, 
 http://www.pps.jussieu.fr/~letouzey/download/rapport_dea.ps.gz
@@ -129,7 +129,7 @@ Types 2002 Post-Workshop Proceedings.
 http://www.pps.jussieu.fr/~letouzey/download/extraction2002.ps.gz
 
 [3]: 
-Programmation fonctionnelle certifiée: l'extraction de programmes
+Programmation fonctionnelle certifiée: l'extraction de programmes
 dans l'assistant Coq. Pierre Letouzey, PhD thesis, 2004.
 http://www.pps.jussieu.fr/~letouzey/download/these_letouzey.ps.gz
 http://www.pps.jussieu.fr/~letouzey/download/these_letouzey_English.ps.gz
diff --git a/plugins/extraction/big.ml b/plugins/extraction/big.ml
index 2fd0e1b5..f2a965c9 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-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \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 558b8359..21819aa8 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,23 +9,20 @@
 open Pp
 open Util
 open Names
-open Term
-open Declarations
 open Namegen
 open Nameops
 open Libnames
+open Globnames
 open Table
 open Miniml
 open Mlutil
-open Modutil
-open Mod_subst
 
 let string_of_id id =
-  let s = Names.string_of_id id in
+  let s = Names.Id.to_string id in
   for i = 0 to String.length s - 2 do
-    if s.[i] = '_' && s.[i+1] = '_' then warning_id s
+    if s.[i] == '_' && s.[i+1] == '_' then warning_id s
   done;
-  ascii_of_ident s
+  Unicode.ascii_of_ident s
 
 let is_mp_bound = function MPbound _ -> true | _ -> false
 
@@ -42,7 +39,7 @@ let pp_apply st par args = match args with
 (** Same as [pp_apply], but with also protection of the head by parenthesis *)
 
 let pp_apply2 st par args =
-  let par' = args <> [] || par in
+  let par' = not (List.is_empty args) || par in
   pp_apply (pp_par par' st) par args
 
 let pr_binding = function
@@ -82,20 +79,20 @@ let is_digit = function
 
 let begins_with_CoqXX s =
   let n = String.length s in
-  n >= 4 && s.[0] = 'C' && s.[1] = 'o' && s.[2] = 'q' &&
+  n >= 4 && s.[0] == 'C' && s.[1] == 'o' && s.[2] == 'q' &&
   let i = ref 3 in
   try while !i < n do
-    if s.[!i] = '_' then i:=n (*Stop*)
+    if s.[!i] == '_' then i:=n (*Stop*)
     else if is_digit s.[!i] then incr i
     else raise Not_found
   done; true
   with Not_found -> false
 
 let unquote s =
-  if lang () <> Scheme then s
+  if lang () != Scheme then s
   else
     let s = String.copy s in
-    for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done;
+    for i=0 to String.length s - 1 do if s.[i] == '\'' then s.[i] <- '~' done;
     s
 
 let rec qualify delim = function
@@ -112,17 +109,28 @@ let pseudo_qualify = qualify "__"
 let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false
 let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false
 
-let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id))
+let lowercase_id id = Id.of_string (String.uncapitalize (string_of_id id))
 let uppercase_id id =
   let s = string_of_id id in
-  assert (s<>"");
-  if s.[0] = '_' then id_of_string ("Coq_"^s)
-  else id_of_string (String.capitalize s)
+  assert (not (String.is_empty s));
+  if s.[0] == '_' then Id.of_string ("Coq_"^s)
+  else Id.of_string (String.capitalize s)
 
 type kind = Term | Type | Cons | Mod
 
+module KOrd =
+struct
+  type t = kind * string
+  let compare (k1, s1) (k2, s2) =
+    let c = Pervasives.compare k1 k2 (** OK *) in
+    if c = 0 then String.compare s1 s2
+    else c
+end
+
+module KMap = Map.Make(KOrd)
+
 let upperkind = function
-  | Type -> lang () = Haskell
+  | Type -> lang () == Haskell
   | Term -> false
   | Cons | Mod -> true
 
@@ -131,12 +139,12 @@ let kindcase_id k id =
 
 (*s de Bruijn environments for programs *)
 
-type env = identifier list * Idset.t
+type env = Id.t list * Id.Set.t
 
 (*s Generic renaming issues for local variable names. *)
 
 let rec rename_id id avoid =
-  if Idset.mem id avoid then rename_id (lift_subscript id) avoid else id
+  if Id.Set.mem id avoid then rename_id (lift_subscript id) avoid else id
 
 let rec rename_vars avoid = function
   | [] ->
@@ -148,14 +156,14 @@ let rec rename_vars avoid = function
   | id :: idl ->
       let (idl, avoid) = rename_vars avoid idl in
       let id = rename_id (lowercase_id id) avoid in
-      (id :: idl, Idset.add id avoid)
+      (id :: idl, Id.Set.add id avoid)
 
 let rename_tvars avoid l =
   let rec rename avoid = function
     | [] -> [],avoid
     | id :: idl ->
 	let id = rename_id (lowercase_id id) avoid in
-	let idl, avoid = rename (Idset.add id avoid) idl in
+	let idl, avoid = rename (Id.Set.add id avoid) idl in
 	(id :: idl, avoid) in
   fst (rename avoid l)
 
@@ -165,7 +173,7 @@ let push_vars ids (db,avoid) =
 
 let get_db_name n (db,_) =
   let id = List.nth db (pred n) in
-  if id = dummy_name then id_of_string "__" else id
+  if Id.equal id dummy_name then Id.of_string "__" else id
 
 
 (*S Renamings of global objects. *)
@@ -182,37 +190,44 @@ let set_phase, get_phase =
   let ph = ref Impl in ((:=) ph), (fun () -> !ph)
 
 let set_keywords, get_keywords =
-  let k = ref Idset.empty in
+  let k = ref Id.Set.empty in
   ((:=) k), (fun () -> !k)
 
 let add_global_ids, get_global_ids =
-  let ids = ref Idset.empty in
+  let ids = ref Id.Set.empty in
   register_cleanup (fun () -> ids := get_keywords ());
-  let add s = ids := Idset.add s !ids
+  let add s = ids := Id.Set.add s !ids
   and get () = !ids
   in (add,get)
 
 let empty_env () = [], get_global_ids ()
 
-let mktable autoclean =
-  let h = Hashtbl.create 97 in
-  if autoclean then register_cleanup (fun () -> Hashtbl.clear h);
-  (Hashtbl.replace h, Hashtbl.find h, fun () -> Hashtbl.clear h)
-
 (* We might have built [global_reference] whose canonical part is
    inaccurate. We must hence compare only the user part,
    hence using a Hashtbl might be incorrect *)
 
+let mktable_id autoclean =
+  let m = ref Id.Map.empty in
+  let clear () = m := Id.Map.empty in
+  if autoclean then register_cleanup clear;
+  (fun r v -> m := Id.Map.add r v !m), (fun r -> Id.Map.find r !m), clear
+
 let mktable_ref autoclean =
   let m = ref Refmap'.empty in
   let clear () = m := Refmap'.empty in
   if autoclean then register_cleanup clear;
   (fun r v -> m := Refmap'.add r v !m), (fun r -> Refmap'.find r !m), clear
 
+let mktable_modpath autoclean =
+  let m = ref MPmap.empty in
+  let clear () = m := MPmap.empty in
+  if autoclean then register_cleanup clear;
+  (fun r v -> m := MPmap.add r v !m), (fun r -> MPmap.find r !m), clear
+
 (* A table recording objects in the first level of all MPfile *)
 
 let add_mpfiles_content,get_mpfiles_content,clear_mpfiles_content =
-  mktable false
+  mktable_modpath false
 
 let get_mpfiles_content mp =
   try get_mpfiles_content mp
@@ -258,7 +273,7 @@ let params_ren_add, params_ren_mem =
 
 type visible_layer = { mp : module_path;
 		       params : module_path list;
-		       content : ((kind*string),label) Hashtbl.t }
+		       mutable content : Label.t KMap.t; }
 
 let pop_visible, push_visible, get_visible =
   let vis = ref [] in
@@ -269,35 +284,47 @@ let pop_visible, push_visible, get_visible =
       | v :: vl ->
 	  vis := vl;
 	  (* we save the 1st-level-content of MPfile for later use *)
-	  if get_phase () = Impl && modular () && is_modfile v.mp
+	  if get_phase () == Impl && modular () && is_modfile v.mp
 	  then add_mpfiles_content v.mp v.content
   and push mp mps =
-    vis := { mp = mp; params = mps; content = Hashtbl.create 97 } :: !vis
+    vis := { mp = mp; params = mps; content = KMap.empty } :: !vis
   and get () = !vis
   in (pop,push,get)
 
 let get_visible_mps () = List.map (function v -> v.mp) (get_visible ())
 let top_visible () = match get_visible () with [] -> assert false | v::_ -> v
 let top_visible_mp () = (top_visible ()).mp
-let add_visible ks l = Hashtbl.add (top_visible ()).content ks l
+let add_visible ks l =
+  let visible = top_visible () in
+  visible.content <- KMap.add ks l visible.content
 
 (* table of local module wrappers used to provide non-ambiguous names *)
 
+module DupOrd =
+struct
+  type t = ModPath.t * Label.t
+  let compare (mp1, l1) (mp2, l2) =
+    let c = Label.compare l1 l2 in
+    if Int.equal c 0 then ModPath.compare mp1 mp2 else c
+end
+
+module DupMap = Map.Make(DupOrd)
+
 let add_duplicate, check_duplicate =
-  let index = ref 0 and dups = ref Gmap.empty in
-  register_cleanup (fun () -> index := 0; dups := Gmap.empty);
+  let index = ref 0 and dups = ref DupMap.empty in
+  register_cleanup (fun () -> index := 0; dups := DupMap.empty);
   let add mp l =
      incr index;
-     let ren = "Coq__" ^ string_of_int (!index) in
-     dups := Gmap.add (mp,l) ren !dups
-  and check mp l = Gmap.find (mp, l) !dups
+     let ren = "Coq__" ^ string_of_int !index in
+     dups := DupMap.add (mp,l) ren !dups
+  and check mp l = DupMap.find (mp, l) !dups
   in (add,check)
 
 type reset_kind = AllButExternal | Everything
 
 let reset_renaming_tables flag =
   do_cleanup ();
-  if flag = Everything then clear_mpfiles_content ()
+  if flag == Everything then clear_mpfiles_content ()
 
 (*S Renaming functions *)
 
@@ -312,8 +339,8 @@ let modular_rename k id =
     if upperkind k then "Coq_",is_upper else "coq_",is_lower
   in
   if not (is_ok s) ||
-    (Idset.mem id (get_keywords ())) ||
-    (String.length s >= 4 && String.sub s 0 4 = prefix)
+    (Id.Set.mem id (get_keywords ())) ||
+    (String.length s >= 4 && String.equal (String.sub s 0 4) prefix)
   then prefix ^ s
   else s
 
@@ -321,10 +348,10 @@ let modular_rename k id =
     with unique numbers *)
 
 let modfstlev_rename =
-  let add_prefixes,get_prefixes,_ = mktable true in
+  let add_prefixes,get_prefixes,_ = mktable_id true in
   fun l ->
-    let coqid = id_of_string "Coq" in
-    let id = id_of_label l in
+    let coqid = Id.of_string "Coq" in
+    let id = Label.to_id l in
     try
       let coqset = get_prefixes id in
       let nextcoq = next_ident_away coqid coqset in
@@ -343,23 +370,26 @@ let rec mp_renaming_fun mp = match mp with
   | _ when not (modular ()) && at_toplevel mp -> [""]
   | MPdot (mp,l) ->
       let lmp = mp_renaming mp in
-      if lmp = [""] then (modfstlev_rename l)::lmp
-      else (modular_rename Mod (id_of_label l))::lmp
+      let mp = match lmp with
+      | [""] -> modfstlev_rename l
+      | _ -> modular_rename Mod (Label.to_id l)
+      in
+      mp ::lmp
   | MPbound mbid ->
-      let s = modular_rename Mod (id_of_mbid mbid) in
+      let s = modular_rename Mod (MBId.to_id mbid) in
       if not (params_ren_mem mp) then [s]
-      else let i,_,_ = repr_mbid mbid in [s^"__"^string_of_int i]
+      else let i,_,_ = MBId.repr mbid in [s^"__"^string_of_int i]
   | MPfile _ ->
       assert (modular ()); (* see [at_toplevel] above *)
-      assert (get_phase () = Pre);
-      let current_mpfile = (list_last (get_visible ())).mp in
-      if mp <> current_mpfile then mpfiles_add mp;
+      assert (get_phase () == Pre);
+      let current_mpfile = (List.last (get_visible ())).mp in
+      if not (ModPath.equal mp current_mpfile) then mpfiles_add mp;
       [string_of_modfile mp]
 
 (* ... and its version using a cache *)
 
 and mp_renaming =
-  let add,get,_ = mktable true in
+  let add,get,_ = mktable_modpath true in
   fun x ->
     try if is_mp_bound (base_mp x) then raise Not_found; get x
     with Not_found -> let y = mp_renaming_fun x in add x y; y
@@ -370,17 +400,17 @@ and mp_renaming =
 let ref_renaming_fun (k,r) =
   let mp = modpath_of_r r in
   let l = mp_renaming mp in
-  let l = if lang () <> Ocaml && not (modular ()) then [""] else l 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
+    match l with
+    | [""] -> (* this happens only at toplevel of the monolithic case *)
+      let globs = Id.Set.elements (get_global_ids ()) in
       let id = next_ident_away (kindcase_id k idg) globs in
       string_of_id id
-    else modular_rename k idg
+    | _ -> modular_rename k idg
   in
-  add_global_ids (id_of_string s);
+  add_global_ids (Id.of_string s);
   s::l
 
 (* Cached version of the last function *)
@@ -399,27 +429,30 @@ let ref_renaming =
 
 let rec clash mem mp0 ks = function
   | [] -> false
-  | mp :: _ when mp = mp0 -> false
+  | mp :: _ when ModPath.equal mp mp0 -> false
   | mp :: _ when mem mp ks -> true
   | _ :: mpl -> clash mem mp0 ks mpl
 
 let mpfiles_clash mp0 ks =
-  clash (fun mp -> Hashtbl.mem (get_mpfiles_content mp)) mp0 ks
+  clash (fun mp k -> KMap.mem k (get_mpfiles_content mp)) mp0 ks
     (List.rev (mpfiles_list ()))
 
 let rec params_lookup mp0 ks = function
   | [] -> false
-  | param :: _ when mp0 = param -> true
+  | param :: _ when ModPath.equal mp0 param -> true
   | param :: params ->
-      if ks = (Mod, List.hd (mp_renaming param)) then params_ren_add param;
+      let () = match ks with
+      | (Mod, mp) when String.equal (List.hd (mp_renaming param)) mp -> params_ren_add param
+      | _ -> ()
+      in
       params_lookup mp0 ks params
 
 let visible_clash mp0 ks =
   let rec clash = function
     | [] -> false
-    | v :: _ when v.mp = mp0 -> false
+    | v :: _ when ModPath.equal v.mp mp0 -> false
     | v :: vis ->
-	let b = Hashtbl.mem v.content ks in
+	let b = KMap.mem ks v.content in
 	if b && not (is_mp_bound mp0) then true
 	else begin
 	  if b then params_ren_add mp0;
@@ -433,9 +466,9 @@ let visible_clash mp0 ks =
 let visible_clash_dbg mp0 ks =
   let rec clash = function
     | [] -> None
-    | v :: _ when v.mp = mp0 -> None
+    | v :: _ when ModPath.equal v.mp mp0 -> None
     | v :: vis ->
-	try Some (v.mp,Hashtbl.find v.content ks)
+	try Some (v.mp,KMap.find ks v.content)
 	with Not_found ->
 	  if params_lookup mp0 ks v.params then None
 	  else clash vis
@@ -455,7 +488,7 @@ let opened_libraries () =
     let to_open =
       List.filter
 	(fun mp ->
-	   not (List.exists (Hashtbl.mem (get_mpfiles_content mp)) used_ks))
+	   not (List.exists (fun k -> KMap.mem k (get_mpfiles_content mp)) used_ks))
 	used_files
     in
     mpfiles_clear ();
@@ -476,7 +509,7 @@ let opened_libraries () =
 
 let pp_duplicate k' prefix mp rls olab =
   let rls', lbl =
-    if k'<>Mod then
+    if k' != Mod then
       (* Here rls=[s], the ref to print is <prefix>.<s>, and olab<>None *)
       rls, Option.get olab
     else
@@ -485,7 +518,7 @@ let pp_duplicate k' prefix mp rls olab =
   in
   try dottify (check_duplicate prefix lbl :: rls')
   with Not_found ->
-    assert (get_phase () = Pre); (* otherwise it's too late *)
+    assert (get_phase () == Pre); (* otherwise it's too late *)
     add_duplicate prefix lbl; dottify rls
 
 let fstlev_ks k = function
@@ -498,8 +531,8 @@ let fstlev_ks k = function
 
 let pp_ocaml_local k prefix mp rls olab =
   (* what is the largest prefix of [mp] that belongs to [visible]? *)
-  assert (k <> Mod || mp <> prefix); (* mp as whole module isn't in itself *)
-  let rls' = list_skipn (mp_length prefix) rls in
+  assert (k != Mod || not (ModPath.equal mp prefix)); (* mp as whole module isn't in itself *)
+  let rls' = List.skipn (mp_length prefix) rls in
   let k's = fstlev_ks k rls' in
   (* Reference r / module path mp is of the form [<prefix>.s.<...>]. *)
   if not (visible_clash prefix k's) then dottify rls'
@@ -510,7 +543,7 @@ let pp_ocaml_local k prefix mp rls olab =
 
 let pp_ocaml_bound base rls =
   (* clash with a MPbound will be detected and fixed by renaming this MPbound *)
-  if get_phase () = Pre then ignore (visible_clash base (Mod,List.hd rls));
+  if get_phase () == Pre then ignore (visible_clash base (Mod,List.hd rls));
   dottify rls
 
 (* [pp_ocaml_extern] : [mp] isn't local, it is defined in another [MPfile]. *)
@@ -519,7 +552,7 @@ let pp_ocaml_extern k base rls = match rls with
   | [] -> assert false
   | base_s :: rls' ->
       if (not (modular ())) (* Pseudo qualification with "" *)
-	|| (rls' = [])  (* Case of a file A.v used as a module later *)
+	|| (List.is_empty rls')  (* Case of a file A.v used as a module later *)
 	|| (not (mpfiles_mem base)) (* Module not opened *)
 	|| (mpfiles_clash base (fstlev_ks k rls')) (* Conflict in opened files *)
 	|| (visible_clash base (fstlev_ks k rls')) (* Local conflict *)
@@ -549,7 +582,7 @@ let pp_haskell_gen k mp rls = match rls with
   | s::rls' ->
     let str = pseudo_qualify rls' in
     let str = if is_upper str && not (upperkind k) then ("_"^str) else str in
-    let prf = if base_mp mp <> top_visible_mp () then s ^ "." else "" in
+    let prf = if not (ModPath.equal (base_mp mp) (top_visible_mp ())) then s ^ "." else "" in
     prf ^ str
 
 (* Main name printing function for a reference *)
@@ -559,7 +592,7 @@ let pp_global k r =
   assert (List.length ls > 1);
   let s = List.hd ls in
   let mp,_,l = repr_of_r r in
-  if mp = top_visible_mp () then
+  if ModPath.equal mp (top_visible_mp ()) then
     (* simpliest situation: definition of r (or use in the same context) *)
     (* we update the visible environment *)
     (add_visible (k,s) l; unquote s)
@@ -575,7 +608,7 @@ let pp_global k r =
 let pp_module mp =
   let ls = mp_renaming mp in
   match mp with
-    | MPdot (mp0,l) when mp0 = top_visible_mp () ->
+    | MPdot (mp0,l) when ModPath.equal mp0 (top_visible_mp ()) ->
 	(* simpliest situation: definition of mp (or use in the same context) *)
 	(* we update the visible environment *)
 	let s = List.hd ls in
@@ -587,7 +620,7 @@ let pp_module mp =
     the constants are directly turned into chars *)
 
 let mk_ind path s =
-  make_mind (MPfile (dirpath_of_string path)) empty_dirpath (mk_label s)
+  MutInd.make2 (MPfile (dirpath_of_string path)) (Label.make s)
 
 let ind_ascii = mk_ind "Coq.Strings.Ascii" "ascii"
 
@@ -598,7 +631,7 @@ let check_extract_ascii () =
       | Haskell -> "Char"
       | _ -> raise Not_found
     in
-    find_custom (IndRef (ind_ascii,0)) = char_type
+    String.equal (find_custom (IndRef (ind_ascii, 0))) (char_type)
   with Not_found -> false
 
 let is_list_cons l =
@@ -606,14 +639,16 @@ let is_list_cons l =
 
 let is_native_char = function
   | MLcons(_,ConstructRef ((kn,0),1),l) ->
-    kn = ind_ascii && check_extract_ascii () && is_list_cons l
+    MutInd.equal kn ind_ascii && check_extract_ascii () && is_list_cons l
   | _ -> false
 
-let pp_native_char c =
+let get_native_char c =
   let rec cumul = function
     | [] -> 0
     | MLcons(_,ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l)
     | _ -> assert false
   in
   let l = match c with MLcons(_,_,l) -> l | _ -> assert false in
-  str ("'"^Char.escaped (Char.chr (cumul l))^"'")
+  Char.chr (cumul l)
+
+let pp_native_char c = str ("'"^Char.escaped (get_native_char c)^"'")
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 7375f2d4..a8ab4fd3 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -1,15 +1,14 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 open Names
-open Libnames
+open Globnames
 open Miniml
-open Mlutil
 open Pp
 
 (** By default, in module Format, you can do horizontal placing of blocks
@@ -33,17 +32,17 @@ 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 pr_binding : Id.t list -> std_ppcmds
 
-val rename_id : identifier -> Idset.t -> identifier
+val rename_id : Id.t -> Id.Set.t -> Id.t
 
-type env = identifier list * Idset.t
+type env = Id.t list * Id.Set.t
 val empty_env : unit -> env
 
-val rename_vars: Idset.t -> identifier list -> env
-val rename_tvars: Idset.t -> identifier list -> identifier list
-val push_vars : identifier list -> env -> identifier list * env
-val get_db_name : int -> env -> identifier
+val rename_vars: Id.Set.t -> Id.t list -> env
+val rename_tvars: Id.Set.t -> Id.t list -> Id.t list
+val push_vars : Id.t list -> env -> Id.t list * env
+val get_db_name : int -> env -> Id.t
 
 type phase = Pre | Impl | Intf
 
@@ -63,13 +62,13 @@ val top_visible_mp : unit -> module_path
 val push_visible : module_path -> module_path list -> unit
 val pop_visible : unit -> unit
 
-val check_duplicate : module_path -> label -> string
+val check_duplicate : module_path -> Label.t -> string
 
 type reset_kind = AllButExternal | Everything
 
 val reset_renaming_tables : reset_kind -> unit
 
-val set_keywords : Idset.t -> unit
+val set_keywords : Id.Set.t -> unit
 
 (** For instance: [mk_ind "Coq.Init.Datatypes" "nat"] *)
 
@@ -80,4 +79,5 @@ val mk_ind : string -> string -> mutual_inductive
     the constants are directly turned into chars *)
 
 val is_native_char : ml_ast -> bool
+val get_native_char : ml_ast -> char
 val pp_native_char : ml_ast -> std_ppcmds
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 84088292..42e69d34 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -1,18 +1,20 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+open Miniml
 open Term
 open Declarations
 open Names
 open Libnames
+open Globnames
 open Pp
+open Errors
 open Util
-open Miniml
 open Table
 open Extraction
 open Modutil
@@ -24,33 +26,41 @@ open Mod_subst
 (***************************************)
 
 let toplevel_env () =
-  let seg = Lib.contents_after None in
   let get_reference = function
     | (_,kn), Lib.Leaf o ->
 	let mp,_,l = repr_kn kn in
-	let seb = match Libobject.object_tag o with
-	  | "CONSTANT" -> SFBconst (Global.lookup_constant (constant_of_kn kn))
-	  | "INDUCTIVE" -> SFBmind (Global.lookup_mind (mind_of_kn kn))
-	  | "MODULE" -> SFBmodule (Global.lookup_module (MPdot (mp,l)))
+	begin match Libobject.object_tag o with
+	  | "CONSTANT" ->
+            let constant = Global.lookup_constant (constant_of_kn kn) in
+            Some (l, SFBconst constant)
+	  | "INDUCTIVE" ->
+            let inductive = Global.lookup_mind (mind_of_kn kn) in
+            Some (l, SFBmind inductive)
+	  | "MODULE" ->
+            let modl = Global.lookup_module (MPdot (mp, l)) in
+            Some (l, SFBmodule modl)
 	  | "MODULE TYPE" ->
-	      SFBmodtype (Global.lookup_modtype (MPdot (mp,l)))
-	  | _ -> failwith "caught"
-	in l,seb
-    | _ -> failwith "caught"
+            let modtype = Global.lookup_modtype (MPdot (mp, l)) in
+            Some (l, SFBmodtype modtype)
+          | "INCLUDE" -> error "No extraction of toplevel Include yet."
+	  | _ -> None
+        end
+    | _ -> None
   in
-  SEBstruct (List.rev (map_succeed get_reference seg))
+  List.rev (List.map_filter get_reference (Lib.contents ()))
 
 
 let environment_until dir_opt =
   let rec parse = function
-    | [] when dir_opt = None -> [current_toplevel (), toplevel_env ()]
+    | [] when Option.is_empty dir_opt -> [Lib.current_mp (), toplevel_env ()]
     | [] -> []
     | d :: 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
+      let meb =
+        Modops.destr_nofunctor (Global.lookup_module (MPfile d)).mod_type
+      in
+      match dir_opt with
+      | Some d' when DirPath.equal d d' -> [MPfile d, meb]
+      | _ -> (MPfile d, meb) :: (parse l)
   in parse (Library.loaded_libraries ())
 
 
@@ -61,16 +71,12 @@ module type VISIT = sig
   (* Reset the dependencies by emptying the visit lists *)
   val reset : unit -> unit
 
-  (* 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 *)
+  (* Add the module_path and all its prefixes to the mp visit list.
+     We'll keep all fields of these modules. *)
   val add_mp_all : module_path -> unit
 
-  (* Add kernel_name / constant / reference / ... in the visit lists.
+  (* Add reference / ... in the visit lists.
      These functions silently add the mp of their arg in the mp list *)
-  val add_ind : mutual_inductive -> unit
-  val add_con : constant -> unit
   val add_ref : global_reference -> unit
   val add_decl_deps : ml_decl -> unit
   val add_spec_deps : ml_spec -> unit
@@ -84,9 +90,6 @@ module type VISIT = sig
 end
 
 module Visit : VISIT = struct
-  (* What used to be in a single KNset should now be split into a KNset
-     (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 mp_all : MPset.t }
@@ -122,6 +125,15 @@ module Visit : VISIT = struct
   let add_spec_deps = spec_iter_references add_ref add_ref add_ref
 end
 
+let add_field_label mp = function
+  | (lab, SFBconst _) -> Visit.add_ref (ConstRef (Constant.make2 mp lab))
+  | (lab, SFBmind _) -> Visit.add_ref (IndRef (MutInd.make2 mp lab, 0))
+  | (lab, (SFBmodule _|SFBmodtype _)) -> Visit.add_mp_all (MPdot (mp,lab))
+
+let rec add_labels mp = function
+  | MoreFunctor (_,_,m) -> add_labels mp m
+  | NoFunctor sign -> List.iter (add_field_label mp) sign
+
 exception Impossible
 
 let check_arity env cb =
@@ -131,31 +143,31 @@ let check_arity env cb =
 let check_fix env cb i =
   match cb.const_body 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)
+	(match kind_of_term (Mod_subst.force_constr lbody) with
+	  | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd)
+	  | CoFix (j,recd) when Int.equal i j -> check_arity env cb; (false,recd)
 	  | _ -> 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
+  Array.equal Name.equal 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
   let n = Array.length (let fi,_,_ = recd in fi) in
-  if n = 1 then [|l|], recd, msb
+  if Int.equal n 1 then [|l|], recd, msb
   else begin
     if List.length msb < n-1 then raise Impossible;
-    let msb', msb'' = list_chop (n-1) msb in
+    let msb', msb'' = List.chop (n-1) msb in
     let labels = Array.make n l in
-    list_iter_i
+    List.iteri
       (fun j ->
 	 function
 	   | (l,SFBconst cb') ->
 	       let check' = check_fix env cb' (j+1) in
-	       if not (fst check = fst check' &&
+	       if not ((fst check : bool) == (fst check') &&
 		   prec_declaration_equal (snd check) (snd check'))
 	       then raise Impossible;
 	       labels.(j+1) <- l;
@@ -163,113 +175,102 @@ let factor_fix env l cb msb =
     labels, recd, msb''
   end
 
-(** Expanding a [struct_expr_body] into a version without abbreviations
+(** Expanding a [module_alg_expr] into a version without abbreviations
     or functor applications. This is done via a detour to entries
     (hack proposed by Elie)
 *)
 
-let rec seb2mse = function
-  | SEBapply (s,s',_) -> Entries.MSEapply(seb2mse s, seb2mse s')
-  | SEBident mp -> Entries.MSEident mp
-  | _ -> failwith "seb2mse: received a non-atomic seb"
-
-let expand_seb env mp seb =
-  let 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
-    instead of the expanded ones. *)
-
-let my_type_of_mb mb =
-  let m0 = mb.mod_type in
-  match mb.mod_type_alg with Some m -> m0,m | None -> m0,m0
-
-let my_type_of_mtb mtb =
-  let m0 = mtb.typ_expr in
-  match mtb.typ_expr_alg with Some m -> m0,m | None -> m0,m0
+let expand_mexpr env mp me =
+  let inl = Some (Flags.get_inline_level()) in
+  let sign,_,_,_ = Mod_typing.translate_mse env (Some mp) inl me in
+  sign
 
 (** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def].
     To check with Elie. *)
 
-let rec msid_of_seb = function
-  | SEBident mp -> mp
-  | SEBwith (seb,_) -> msid_of_seb seb
+let rec mp_of_mexpr = function
+  | MEident mp -> mp
+  | MEwith (seb,_) -> mp_of_mexpr seb
   | _ -> assert false
 
-let env_for_mtb_with_def env mp seb idl =
-  let sig_b = match seb with
-    | SEBstruct(sig_b) -> sig_b
-    | _ -> assert false
-  in
-  let l = label_of_id (List.hd idl) in
-  let spot = function (l',SFBconst _) -> l = l' | _ -> false in
-  let before = fst (list_split_when spot sig_b) in
-  Modops.add_signature mp before empty_delta_resolver env
+let env_for_mtb_with_def env mp me idl =
+  let struc = Modops.destr_nofunctor me in
+  let l = Label.of_id (List.hd idl) in
+  let spot = function (l',SFBconst _) -> Label.equal l l' | _ -> false in
+  let before = fst (List.split_when spot struc) in
+  Modops.add_structure mp before empty_delta_resolver env
 
 (* From a [structure_body] (i.e. a list of [structure_field_body])
    to specifications. *)
 
-let rec extract_sfb_spec env mp = function
+let rec extract_structure_spec env mp = function
   | [] -> []
   | (l,SFBconst cb) :: msig ->
-      let kn = make_con mp empty_dirpath l in
+      let kn = Constant.make2 mp l in
       let s = extract_constant_spec env kn cb in
-      let specs = extract_sfb_spec env mp msig in
+      let specs = extract_structure_spec env mp msig in
       if logical_spec s then specs
       else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
   | (l,SFBmind _) :: msig ->
-      let mind = make_mind mp empty_dirpath l in
+      let mind = MutInd.make2 mp l in
       let s = Sind (mind, extract_inductive env mind) in
-      let specs = extract_sfb_spec env mp msig in
+      let specs = extract_structure_spec env mp msig in
       if logical_spec s then specs
       else begin Visit.add_spec_deps s; (l,Spec s) :: specs end
   | (l,SFBmodule mb) :: msig ->
-      let specs = extract_sfb_spec env mp msig in
-      let spec = extract_seb_spec env mb.mod_mp (my_type_of_mb mb) in
+      let specs = extract_structure_spec env mp msig in
+      let spec = extract_mbody_spec env mb.mod_mp mb in
       (l,Smodule spec) :: specs
   | (l,SFBmodtype mtb) :: msig ->
-      let specs = extract_sfb_spec env mp msig in
-      let spec = extract_seb_spec env mtb.typ_mp (my_type_of_mtb mtb) in
+      let specs = extract_structure_spec env mp msig in
+      let spec = extract_mbody_spec env mtb.mod_mp mtb in
       (l,Smodtype spec) :: specs
 
-(* From [struct_expr_body] to specifications *)
+(* From [module_expression] to specifications *)
 
-(* Invariant: the [seb] given to [extract_seb_spec] should either come
+(* Invariant: the [me] given to [extract_mexpr_spec] should either come
    from a [mod_type] or [type_expr] field, or their [_alg] counterparts.
-   This way, any encountered [SEBident] should be a true module type.
+   This way, any encountered [MEident] should be a true module type.
 *)
 
-and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with
-  | SEBident mp -> Visit.add_mp_all mp; MTident mp
-  | SEBwith(seb',With_definition_body(idl,cb))->
-      let env' = env_for_mtb_with_def env (msid_of_seb seb') seb idl in
-      let mt = extract_seb_spec env mp1 (seb,seb') in
-      (match extract_with_type env' cb with (* cb peut contenir des kn  *)
+and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with
+  | MEident mp -> Visit.add_mp_all mp; MTident mp
+  | MEwith(me',WithDef(idl,c))->
+      let env' = env_for_mtb_with_def env (mp_of_mexpr me') me_struct idl in
+      let mt = extract_mexpr_spec env mp1 (me_struct,me') in
+      (match extract_with_type env' c with (* cb may contain some kn *)
 	 | None -> mt
 	 | Some (vl,typ) -> MTwith(mt,ML_With_type(idl,vl,typ)))
-  | SEBwith(seb',With_module_body(idl,mp))->
+  | MEwith(me',WithMod(idl,mp))->
       Visit.add_mp_all mp;
-      MTwith(extract_seb_spec env mp1 (seb,seb'),
-	     ML_With_module(idl,mp))
-  | SEBfunctor (mbid, mtb, seb_alg') ->
-      let seb' = match seb with
-	| SEBfunctor (mbid',_,seb') when mbid' = mbid -> seb'
+      MTwith(extract_mexpr_spec env mp1 (me_struct,me'), ML_With_module(idl,mp))
+  | MEapply _ -> extract_msignature_spec env mp1 me_struct
+
+and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with
+  | MoreFunctor (mbid, mtb, me_alg') ->
+      let me_struct' = match me_struct with
+	| MoreFunctor (mbid',_,me') when MBId.equal mbid' mbid -> me'
 	| _ -> assert false
       in
       let mp = MPbound mbid in
-      let env' = Modops.add_module (Modops.module_body_of_type mp mtb) env in
-      MTfunsig (mbid, extract_seb_spec env mp (my_type_of_mtb mtb),
-		extract_seb_spec env' mp1 (seb',seb_alg'))
-  | SEBstruct (msig) ->
-      let env' = Modops.add_signature mp1 msig empty_delta_resolver env in
-      MTsig (mp1, extract_sfb_spec env' mp1 msig)
-  | SEBapply _ ->
-      if seb <> seb_alg then extract_seb_spec env mp1 (seb,seb)
-      else assert false
-
+      let env' = Modops.add_module_type mp mtb env in
+      MTfunsig (mbid, extract_mbody_spec env mp mtb,
+		extract_mexpression_spec env' mp1 (me_struct',me_alg'))
+  | NoFunctor m -> extract_mexpr_spec env mp1 (me_struct,m)
+
+and extract_msignature_spec env mp1 = function
+  | NoFunctor struc ->
+      let env' = Modops.add_structure mp1 struc empty_delta_resolver env in
+      MTsig (mp1, extract_structure_spec env' mp1 struc)
+  | MoreFunctor (mbid, mtb, me) ->
+      let mp = MPbound mbid in
+      let env' = Modops.add_module_type mp mtb env in
+      MTfunsig (mbid, extract_mbody_spec env mp mtb,
+		extract_msignature_spec env' mp1 me)
 
+and extract_mbody_spec env mp mb = match mb.mod_type_alg with
+  | Some ty -> extract_mexpression_spec env mp (mb.mod_type,ty)
+  | None -> extract_msignature_spec env mp mb.mod_type
 
 (* From a [structure_body] (i.e. a list of [structure_field_body])
    to implementations.
@@ -278,88 +279,117 @@ and extract_seb_spec env mp1 (seb,seb_alg) = match seb_alg with
    important: last to first ensures correct dependencies.
 *)
 
-let rec extract_sfb env mp all = function
+let rec extract_structure env mp ~all = function
   | [] -> []
-  | (l,SFBconst cb) :: msb ->
+  | (l,SFBconst cb) :: struc ->
       (try
-	 let vl,recd,msb = factor_fix env l cb msb in
-	 let vc = Array.map (make_con mp empty_dirpath) vl in
-	 let ms = extract_sfb env mp all msb in
-	 let b = array_exists Visit.needed_con vc in
+	 let vl,recd,struc = factor_fix env l cb struc in
+	 let vc = Array.map (Constant.make2 mp) vl in
+	 let ms = extract_structure env mp ~all struc in
+	 let b = Array.exists Visit.needed_con vc in
 	 if all || b then
 	   let d = extract_fixpoint env vc recd in
 	   if (not b) && (logical_decl d) then ms
 	   else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
 	 else ms
        with Impossible ->
-	 let ms = extract_sfb env mp all msb in
-	 let c = make_con mp empty_dirpath l in
+	 let ms = extract_structure env mp ~all struc in
+	 let c = Constant.make2 mp l in
 	 let b = Visit.needed_con c in
 	 if all || b then
 	   let d = extract_constant env c cb in
 	   if (not b) && (logical_decl d) then ms
 	   else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
 	 else ms)
-  | (l,SFBmind mib) :: msb ->
-      let ms = extract_sfb env mp all msb in
-      let mind = make_mind mp empty_dirpath l in
+  | (l,SFBmind mib) :: struc ->
+      let ms = extract_structure env mp ~all struc in
+      let mind = MutInd.make2 mp l in
       let b = Visit.needed_ind mind in
       if all || b then
 	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
-  | (l,SFBmodule mb) :: msb ->
-      let ms = extract_sfb env mp all msb in
+  | (l,SFBmodule mb) :: struc ->
+      let ms = extract_structure env mp ~all struc in
       let mp = MPdot (mp,l) in
-      if all || Visit.needed_mp mp then
-	(l,SEmodule (extract_module env mp true mb)) :: ms
+      let all' = all || Visit.needed_mp_all mp in
+      if all' || Visit.needed_mp mp then
+	(l,SEmodule (extract_module env mp ~all:all' mb)) :: ms
       else ms
-  | (l,SFBmodtype mtb) :: msb ->
-      let ms = extract_sfb env mp all msb in
+  | (l,SFBmodtype mtb) :: struc ->
+      let ms = extract_structure env mp ~all struc in
       let mp = MPdot (mp,l) in
-       if all || Visit.needed_mp mp then
-	(l,SEmodtype (extract_seb_spec env mp (my_type_of_mtb mtb))) :: ms
+      if all || Visit.needed_mp mp then
+        (l,SEmodtype (extract_mbody_spec env mp mtb)) :: ms
       else ms
 
-(* From [struct_expr_body] to implementations *)
+(* From [module_expr] and [module_expression] to implementations *)
 
-and extract_seb env mp all = function
-  | (SEBident _ | SEBapply _) as seb when lang () <> Ocaml ->
-      (* in Haskell/Scheme, we expand everything *)
-      extract_seb env mp all (expand_seb env mp seb)
-  | SEBident mp ->
+and extract_mexpr env mp = function
+  | MEwith _ -> assert false (* no 'with' syntax for modules *)
+  | me when lang () != Ocaml ->
+      (* In Haskell/Scheme, we expand everything.
+         For now, we also extract everything, dead code will be removed later
+         (see [Modutil.optimize_struct]. *)
+      extract_msignature env mp ~all:true (expand_mexpr env mp me)
+  | MEident mp ->
       if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false;
-      Visit.add_mp_all mp; MEident mp
-  | SEBapply (meb, meb',_) ->
-      MEapply (extract_seb env mp true meb,
-	       extract_seb env mp true meb')
-  | SEBfunctor (mbid, mtb, meb) ->
+      Visit.add_mp_all mp; Miniml.MEident mp
+  | MEapply (me, arg) ->
+      Miniml.MEapply (extract_mexpr env mp me,
+	              extract_mexpr env mp (MEident arg))
+
+and extract_mexpression env mp = function
+  | NoFunctor me -> extract_mexpr env mp me
+  | MoreFunctor (mbid, mtb, me) ->
+      let mp1 = MPbound mbid in
+      let env' = Modops.add_module_type mp1 mtb	env in
+      Miniml.MEfunctor
+        (mbid,
+         extract_mbody_spec env mp1 mtb,
+	 extract_mexpression env' mp me)
+
+and extract_msignature env mp ~all = function
+  | NoFunctor struc ->
+      let env' = Modops.add_structure mp struc empty_delta_resolver env in
+      Miniml.MEstruct (mp,extract_structure env' mp ~all struc)
+  | MoreFunctor (mbid, mtb, me) ->
       let mp1 = MPbound mbid in
-      let env' = Modops.add_module (Modops.module_body_of_type  mp1 mtb)
-	env  in
-      MEfunctor (mbid, extract_seb_spec env mp1 (my_type_of_mtb mtb),
-		 extract_seb env' mp true meb)
-  | SEBstruct (msb) ->
-      let env' = Modops.add_signature mp msb empty_delta_resolver env in
-      MEstruct (mp,extract_sfb env' mp all msb)
-  | SEBwith (_,_) -> anomaly "Not available yet"
-
-and extract_module env mp all mb =
+      let env' = Modops.add_module_type mp1 mtb	env in
+      Miniml.MEfunctor
+        (mbid,
+         extract_mbody_spec env mp1 mtb,
+	 extract_msignature env' mp ~all me)
+
+and extract_module env mp ~all mb =
   (* A module has an empty [mod_expr] when :
      - it is a module variable (for instance X inside a Module F [X:SIG])
      - it is a module assumption (Declare Module).
      Since we look at modules from outside, we shouldn't have variables.
      But a Declare Module at toplevel seems legal (cf #2525). For the
      moment we don't support this situation. *)
-  match mb.mod_expr with
-    | None -> error_no_module_expr mp
-    | Some me ->
-      { ml_mod_expr = extract_seb env mp all me;
-	ml_mod_type = extract_seb_spec env mp (my_type_of_mb mb) }
-
-
-let unpack = function MEstruct (_,sel) -> sel | _ -> assert false
+  let impl = match mb.mod_expr with
+    | Abstract -> error_no_module_expr mp
+    | Algebraic me -> extract_mexpression env mp me
+    | Struct sign ->
+      (* This module has a signature, otherwise it would be FullStruct.
+         We extract just the elements required by this signature. *)
+      let () = add_labels mp mb.mod_type in
+      extract_msignature env mp ~all:false sign
+    | FullStruct -> extract_msignature env mp ~all mb.mod_type
+  in
+  (* Slight optimization: for modules without explicit signatures
+     ([FullStruct] case), we build the type out of the extracted
+     implementation *)
+  let typ = match mb.mod_expr with
+    | FullStruct ->
+      assert (Option.is_empty mb.mod_type_alg);
+      mtyp_of_mexpr impl
+    | _ -> extract_mbody_spec env mp mb
+  in
+  { ml_mod_expr = impl;
+    ml_mod_type = typ }
 
 let mono_environment refs mpl =
   Visit.reset ();
@@ -368,7 +398,8 @@ let mono_environment refs 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 (Visit.needed_mp_all mp) m))
+    (fun (mp,struc) ->
+      mp, extract_structure env mp ~all:(Visit.needed_mp_all mp) struc)
     l
 
 (**************************************)
@@ -383,7 +414,7 @@ let descr () = match lang () with
 (* From a filename string "foo.ml" or "foo", builds "foo.ml" and "foo.mli"
    Works similarly for the other languages. *)
 
-let default_id = id_of_string "Main"
+let default_id = Id.of_string "Main"
 
 let mono_filename f =
   let d = descr () in
@@ -396,10 +427,10 @@ let mono_filename f =
 	  else f
 	in
 	let id =
-	  if lang () <> Haskell then default_id
+	  if lang () != Haskell then default_id
 	  else
-            try id_of_string (Filename.basename f)
-	    with e when Errors.noncritical e ->
+            try Id.of_string (Filename.basename f)
+	    with UserError _ ->
               error "Extraction: provided filename is not a valid identifier"
 	in
 	Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id
@@ -409,7 +440,7 @@ let mono_filename f =
 let module_filename mp =
   let f = file_of_modfile mp in
   let d = descr () in
-  Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id_of_string f
+  Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, Id.of_string f
 
 (*s Extraction of one decl to stdout. *)
 
@@ -420,8 +451,9 @@ let print_one_decl struc mp decl =
   ignore (d.pp_struct struc);
   set_phase Impl;
   push_visible mp [];
-  msgnl (d.pp_decl decl);
-  pop_visible ()
+  let ans = d.pp_decl decl in
+  pop_visible ();
+  ans
 
 (*s Extraction of a ml struct to a file. *)
 
@@ -449,31 +481,39 @@ let formatter dry file =
       (* note: max_indent should be < margin above, otherwise it's ignored *)
   ft
 
+let get_comment () =
+  let s = file_comment () in
+  if String.is_empty s then None
+  else
+    let split_comment = Str.split (Str.regexp "[ \t\n]+") s in
+    Some (prlist_with_sep spc str split_comment)
+
 let print_structure_to_file (fn,si,mo) dry struc =
   Buffer.clear buf;
   let d = descr () in
   reset_renaming_tables AllButExternal;
   let unsafe_needs = {
-    mldummy = struct_ast_search ((=) MLdummy) struc;
+    mldummy = struct_ast_search ((==) MLdummy) struc;
     tdummy = struct_type_search Mlutil.isDummy struc;
-    tunknown = struct_type_search ((=) Tunknown) struc;
+    tunknown = struct_type_search ((==) Tunknown) struc;
     magic =
-      if lang () <> Haskell then false
+      if lang () != Haskell then false
       else struct_ast_search (function MLmagic _ -> true | _ -> false) struc }
   in
   (* First, a dry run, for computing objects to rename or duplicate *)
   set_phase Pre;
   let devnull = formatter true None in
-  msg_with devnull (d.pp_struct struc);
+  pp_with devnull (d.pp_struct struc);
   let opened = opened_libraries () in
   (* Print the implementation *)
   let cout = if dry then None else Option.map open_out fn in
   let ft = formatter dry cout in
+  let comment = get_comment () in
   begin try
     (* The real printing of the implementation *)
     set_phase Impl;
-    msg_with ft (d.preamble mo opened unsafe_needs);
-    msg_with ft (d.pp_struct struc);
+    pp_with ft (d.preamble mo comment opened unsafe_needs);
+    pp_with ft (d.pp_struct struc);
     Option.iter close_out cout;
   with reraise ->
     Option.iter close_out cout; raise reraise
@@ -486,8 +526,8 @@ let print_structure_to_file (fn,si,mo) dry struc =
        let ft = formatter false (Some cout) in
        begin try
 	 set_phase Intf;
-	 msg_with ft (d.sig_preamble mo opened unsafe_needs);
-	 msg_with ft (d.pp_sig (signature_of_structure struc));
+	 pp_with ft (d.sig_preamble mo comment opened unsafe_needs);
+	 pp_with ft (d.pp_sig (signature_of_structure struc));
 	 close_out cout;
        with reraise ->
 	 close_out cout; raise reraise
@@ -495,8 +535,8 @@ let print_structure_to_file (fn,si,mo) dry struc =
        info_file si)
     (if dry then None else si);
   (* Print the buffer content via Coq standard formatter (ok with coqide). *)
-  if Buffer.length buf <> 0 then begin
-    Pp.message (Buffer.contents buf);
+  if not (Int.equal (Buffer.length buf) 0) then begin
+    Pp.msg_info (str (Buffer.contents buf));
     Buffer.reset buf
   end
 
@@ -515,7 +555,7 @@ let init modular library =
   set_modular modular;
   set_library library;
   reset ();
-  if modular && lang () = Scheme then error_scheme ()
+  if modular && lang () == Scheme then error_scheme ()
 
 let warns () =
   warning_opaques (access_opaque ());
@@ -531,7 +571,7 @@ let rec locate_ref = function
       let mpo = try Some (Nametab.locate_module q) with Not_found -> None
       and ro =
         try Some (Smartlocate.global_with_alias r)
-        with e when Errors.noncritical e -> None
+        with Nametab.GlobalizationError _ | UserError _ -> None
       in
       match mpo, ro with
 	| None, None -> Nametab.error_global_not_found q
@@ -576,7 +616,7 @@ let separate_extraction lr =
     is \verb!Extraction! [qualid]. *)
 
 let simple_extraction r =
-  Vernacentries.dump_global (Genarg.AN r);
+  Vernacentries.dump_global (Misctypes.AN r);
   match locate_ref [r] with
   | ([], [mp]) as p -> full_extr None p
   | [r],[] ->
@@ -584,9 +624,13 @@ let simple_extraction r =
       let struc = optimize_struct ([r],[]) (mono_environment [r] []) in
       let d = get_decl_in_structure r struc in
       warns ();
-      if is_custom r then msgnl (str "(** User defined extraction *)");
-      print_one_decl struc (modpath_of_r r) d;
-      reset ()
+      let flag =
+        if is_custom r then str "(** User defined extraction *)" ++ fnl()
+        else mt ()
+      in
+      let ans = flag ++ print_one_decl struc (modpath_of_r r) d in
+      reset ();
+      Pp.msg_info ans
   | _ -> assert false
 
 
@@ -602,9 +646,9 @@ let extraction_library is_rec 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) =
+  let select l (mp,struc) =
     if Visit.needed_mp mp
-    then (mp, unpack (extract_seb env mp true meb)) :: l
+    then (mp, extract_structure env mp true struc) :: l
     else l
   in
   let struc = List.fold_left select [] l in
@@ -612,9 +656,22 @@ let extraction_library is_rec m =
   warns ();
   let print = function
     | (MPfile dir as mp, sel) as e ->
-	let dry = not is_rec && dir <> dir_m in
+	let dry = not is_rec && not (DirPath.equal dir dir_m) in
 	print_structure_to_file (module_filename mp) dry [e]
     | _ -> assert false
   in
   List.iter print struc;
   reset ()
+
+let structure_for_compute c =
+  init false false;
+  let env = Global.env () in
+  let ast, mlt = Extraction.extract_constr env c in
+  let ast = Mlutil.normalize ast in
+  let refs = ref Refset.empty in
+  let add_ref r = refs := Refset.add r !refs in
+  let () = ast_iter_references add_ref add_ref add_ref ast in
+  let refs = Refset.elements !refs in
+  let struc = optimize_struct (refs,[]) (mono_environment refs []) in
+  let flatstruc = List.map snd (List.flatten (List.map snd struc)) in
+  flatstruc, ast, mlt
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 31f5a620..e5fe76f5 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -10,11 +10,12 @@
 
 open Names
 open Libnames
+open Globnames
 
 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
+val extraction_library : bool -> Id.t -> unit
 
 (* For debug / external output via coqtop.byte + Drop : *)
 
@@ -24,4 +25,10 @@ val mono_environment :
 (* Used by the Relation Extraction plugin *)
 
 val print_one_decl :
-  Miniml.ml_structure -> module_path -> Miniml.ml_decl -> unit
+  Miniml.ml_structure -> module_path -> Miniml.ml_decl -> Pp.std_ppcmds
+
+(* Used by Extraction Compute *)
+
+val structure_for_compute :
+  Term.constr ->
+    Miniml.ml_flat_structure * Miniml.ml_ast * Miniml.ml_type
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index a5b1e3c6..080512b2 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -10,7 +10,10 @@
 open Util
 open Names
 open Term
+open Vars
+open Context
 open Declarations
+open Declareops
 open Environ
 open Reduction
 open Reductionops
@@ -19,9 +22,7 @@ open Termops
 open Inductiveops
 open Recordops
 open Namegen
-open Summary
-open Libnames
-open Nametab
+open Globnames
 open Miniml
 open Table
 open Mlutil
@@ -36,13 +37,13 @@ let none = Evd.empty
 
 let type_of env c =
   try
-    let polyprop = (lang() = Haskell) in
+    let polyprop = (lang() == Haskell) in
     Retyping.get_type_of ~polyprop env none (strip_outer_cast c)
   with SingletonInductiveBecomesProp id -> error_singleton_become_prop id
 
 let sort_of env c =
   try
-    let polyprop = (lang() = Haskell) in
+    let polyprop = (lang() == Haskell) in
     Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c)
   with SingletonInductiveBecomesProp id -> error_singleton_become_prop id
 
@@ -55,8 +56,8 @@ let sort_of env c =
      More formally, a type scheme has type $(x_1:X_1)\ldots(x_n:X_n)s$ with
      [s = Set], [Prop] or [Type]
    \item [Default] denotes the other cases. It may be inexact after
-     instanciation. For example [(X:Type)X] is [Default] and may give [Set]
-     after instanciation, which is rather [TypeScheme]
+     instantiation. For example [(X:Type)X] is [Default] and may give [Set]
+     after instantiation, which is rather [TypeScheme]
    \item [Logic] denotes a term of sort [Prop], or a type scheme on sort [Prop]
    \item [Info] is the opposite. The same example [(X:Type)X] shows
      that an [Info] term might in fact be [Logic] later on.
@@ -71,17 +72,19 @@ type flag = info * scheme
 (*s [flag_of_type] transforms a type [t] into a [flag].
   Really important function. *)
 
-let rec flag_of_type env t =
+let rec flag_of_type env t : flag =
   let t = whd_betadeltaiota env none t in
   match kind_of_term t with
     | Prod (x,t,c) -> flag_of_type (push_rel (x,None,t) env) c
-    | Sort (Prop Null) -> (Logic,TypeScheme)
+    | Sort s when Sorts.is_prop s -> (Logic,TypeScheme)
     | Sort _ -> (Info,TypeScheme)
-    | _ -> if (sort_of env t) = InProp then (Logic,Default) else (Info,Default)
+    | _ -> if (sort_of env t) == InProp then (Logic,Default) else (Info,Default)
 
 (*s Two particular cases of [flag_of_type]. *)
 
-let is_default env t = (flag_of_type env t = (Info, Default))
+let is_default env t = match flag_of_type env t with
+| (Info, Default) -> true
+| _ -> false
 
 exception NotDefault of kill_reason
 
@@ -91,7 +94,9 @@ let check_default env t =
     | Logic,_ -> raise (NotDefault Kother)
     | _ -> ()
 
-let is_info_scheme env t = (flag_of_type env t = (Info, TypeScheme))
+let is_info_scheme env t = match flag_of_type env t with
+| (Info, TypeScheme) -> true
+| _ -> false
 
 (*s [type_sign] gernerates a signature aimed at treating a type application. *)
 
@@ -109,16 +114,31 @@ let rec type_scheme_nb_args env c =
 	if is_info_scheme env t then n+1 else n
     | _ -> 0
 
-let _ = register_type_scheme_nb_args type_scheme_nb_args
+let _ = Hook.set type_scheme_nb_args_hook type_scheme_nb_args
 
 (*s [type_sign_vl] does the same, plus a type var list. *)
 
+(* When generating type variables, we avoid any ' in their names
+   (otherwise this may cause a lexer conflict in ocaml with 'a').
+   We also get rid of unicode characters. Anyway, since type variables
+   are local, the created name is just a matter of taste...
+   See also Bug #3227 *)
+
+let make_typvar n vl =
+  let id = id_of_name n in
+  let id' =
+    let s = Id.to_string id in
+    if not (String.contains s '\'') && Unicode.is_basic_ascii s then id
+    else id_of_name Anonymous
+  in
+  next_ident_away id' vl
+
 let rec type_sign_vl env c =
   match kind_of_term (whd_betadeltaiota env none c) with
     | Prod (n,t,d) ->
 	let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in
 	if not (is_info_scheme env t) then Kill Kother::s, vl
-	else Keep::s, (next_ident_away (id_of_name n) vl) :: vl
+	else Keep::s, (make_typvar n vl) :: vl
     | _ -> [],[]
 
 let rec nb_default_params env c =
@@ -136,7 +156,8 @@ let sign_with_implicits r s nb_params =
     | [] -> []
     | sign::s ->
 	let sign' =
-	  if sign = Keep && List.mem i implicits then Kill Kother else sign
+	  if sign == Keep && Int.List.mem i implicits
+          then Kill Kother else sign
 	in sign' :: add_impl (succ i) s
   in
   add_impl (1+nb_params) s
@@ -145,11 +166,11 @@ let sign_with_implicits r s nb_params =
 
 let rec handle_exn r n fn_name = function
   | MLexn s ->
-      (try Scanf.sscanf s "UNBOUND %d"
+      (try Scanf.sscanf s "UNBOUND %d%!"
 	 (fun i ->
 	    assert ((0 < i) && (i <= n));
 	    MLexn ("IMPLICIT "^ msg_non_implicit r (n+1-i) (fn_name i)))
-       with e when Errors.noncritical e -> MLexn s)
+       with Scanf.Scan_failure _ | End_of_file -> MLexn s)
   | a -> ast_map (handle_exn r n fn_name) a
 
 (*S Management of type variable contexts. *)
@@ -170,8 +191,8 @@ let db_from_sign s =
   an inductive type (see just below). *)
 
 let rec db_from_ind dbmap i =
-  if i = 0 then []
-  else (try Intmap.find i dbmap with Not_found -> 0)::(db_from_ind dbmap (i-1))
+  if Int.equal i 0 then []
+  else (try Int.Map.find i dbmap with Not_found -> 0)::(db_from_ind dbmap (i-1))
 
 (*s [parse_ind_args] builds a map: [i->j] iff the i-th Coq argument
   of a constructor corresponds to the j-th type var of the ML inductive. *)
@@ -185,34 +206,43 @@ let rec db_from_ind dbmap i =
 
 let parse_ind_args si args relmax =
   let rec parse i j = function
-    | [] -> Intmap.empty
+    | [] -> Int.Map.empty
     | Kill _ :: s -> parse (i+1) j s
     | Keep :: s ->
       (match kind_of_term args.(i-1) with
-	 | Rel k -> Intmap.add (relmax+1-k) j (parse (i+1) (j+1) s)
+	 | Rel k -> Int.Map.add (relmax+1-k) j (parse (i+1) (j+1) s)
 	 | _ -> 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
+  Id.equal o1.mind_typename o2.mind_typename &&
+  List.equal eq_rel_declaration o1.mind_arity_ctxt o2.mind_arity_ctxt &&
+    begin
+      match o1.mind_arity, o2.mind_arity with
+      | RegularArity {mind_user_arity=c1; mind_sort=s1}, RegularArity {mind_user_arity=c2; mind_sort=s2} ->
+	eq_constr c1 c2 && Sorts.equal s1 s2
+      | TemplateArity p1, TemplateArity p2 ->
+	let eq o1 o2 = Option.equal Univ.Level.equal o1 o2 in
+	  List.equal eq p1.template_param_levels p2.template_param_levels &&
+	    Univ.Universe.equal p1.template_level p2.template_level
+      | _, _ -> false
+    end &&
+    Array.equal Id.equal o1.mind_consnames o2.mind_consnames
+
+let eq_record x y =
+  Option.equal (Option.equal (fun (_, x, y) (_, x', y') -> Array.for_all2 eq_constant x x')) x y
 
 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
+  Array.equal oib_equal m1.mind_packets m1.mind_packets &&
+  eq_record m1.mind_record m2.mind_record &&
+  (m1.mind_finite : Decl_kinds.recursivity_kind) == m2.mind_finite &&
+  Int.equal m1.mind_ntypes m2.mind_ntypes &&
+  List.equal eq_named_declaration m1.mind_hyps m2.mind_hyps &&
+  Int.equal m1.mind_nparams m2.mind_nparams &&
+  Int.equal m1.mind_nparams_rec m2.mind_nparams_rec &&
+  List.equal eq_rel_declaration m1.mind_params_ctxt m2.mind_params_ctxt &&
+  (* Univ.UContext.eq *) m1.mind_universes == m2.mind_universes (** FIXME *)
+  (* m1.mind_universes = m2.mind_universes *)
 
 (*S Extraction of a type. *)
 
@@ -235,7 +265,7 @@ let rec extract_type env db j c args =
 	   | [] -> 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 = []);
+	assert (List.is_empty args);
 	let env' = push_rel_assum (n,t) env in
 	(match flag_of_type env t with
 	   | (Info, Default) ->
@@ -255,10 +285,10 @@ let rec extract_type env db j c args =
 	       (match expand env mld with
 		  | Tdummy d -> Tdummy d
 		  | _ ->
-		      let reason = if lvl=TypeScheme then Ktype else Kother in
+		      let reason = if lvl == TypeScheme then Ktype else Kother in
 		      Tarr (Tdummy reason, mld)))
     | Sort _ -> Tdummy Ktype (* The two logical cases. *)
-    | _ when sort_of env (applist (c, args)) = InProp -> Tdummy Kother
+    | _ when sort_of env (applist (c, args)) == InProp -> Tdummy Kother
     | Rel n ->
 	(match lookup_rel n env with
            | (_,Some t,_) -> extract_type env db j (lift n t) args
@@ -266,11 +296,11 @@ let rec extract_type env db j c args =
 	       (* Asks [db] a translation for [n]. *)
 	       if n > List.length db then Tunknown
 	       else let n' = List.nth db (n-1) in
-	       if n' = 0 then Tunknown else Tvar n')
-    | Const kn ->
+	       if Int.equal n' 0 then Tunknown else Tvar n')
+    | Const (kn,u as c) ->
 	let r = ConstRef kn in
 	let cb = lookup_constant kn env in
-	let typ = Typeops.type_of_constant_type env cb.const_type in
+	let typ,_ = Typeops.type_of_constant env c in
 	(match flag_of_type env typ with
 	   | (Logic,_) -> assert false (* Cf. logical cases above *)
 	   | (Info, TypeScheme) ->
@@ -279,23 +309,23 @@ let rec extract_type env db j c args =
 		  | Undef _ | OpaqueDef _ -> mlt
 		  | Def _ when is_custom r -> mlt
 		  | Def lbody ->
-		      let newc = applist (Declarations.force lbody, args) in
+		      let newc = applist (Mod_subst.force_constr lbody, args) in
 		      let mlt' = extract_type env db j newc [] in
 		      (* ML type abbreviations interact badly with Coq *)
 		      (* reduction, so [mlt] and [mlt'] might be different: *)
 		      (* The more precise is [mlt'], extracted after reduction *)
 		      (* 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')
+		      if eq_ml_type (expand env mlt) (expand env mlt') then mlt else mlt')
 	   | (Info, Default) ->
                (* Not an ML type, for example [(c:forall X, X->X) Type nat] *)
 	       (match cb.const_body with
 		  | Undef _  | OpaqueDef _ -> Tunknown (* Brutal approx ... *)
 		  | Def lbody ->
 		      (* We try to reduce. *)
-		      let newc = applist (Declarations.force lbody, args) in
+		      let newc = applist (Mod_subst.force_constr lbody, args) in
 		      extract_type env db j newc []))
-    | Ind (kn,i) ->
+    | Ind ((kn,i),u) ->
 	let s = (extract_ind env kn).ind_packets.(i).ip_sign in
 	extract_type_app env db (IndRef (kn,i),s) args
     | Case _ | Fix _ | CoFix _ -> Tunknown
@@ -308,7 +338,7 @@ let rec extract_type env db j c args =
 and extract_type_app env db (r,s) args =
   let ml_args =
     List.fold_right
-      (fun (b,c) a -> if b=Keep then
+      (fun (b,c) a -> if b == Keep then
 	 let p = List.length (fst (splay_prod env none (type_of env c))) in
          let db = iterate (fun l -> 0 :: l) p db in
          (extract_type_scheme env db c p) :: a
@@ -326,7 +356,7 @@ and extract_type_app env db (r,s) args =
 (* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *)
 
 and extract_type_scheme env db c p =
-  if p=0 then extract_type env db 0 c []
+  if Int.equal p 0 then extract_type env db 0 c []
   else
     let c = whd_betaiotazeta Evd.empty c in
     match kind_of_term c with
@@ -335,7 +365,7 @@ and extract_type_scheme env db c p =
       | _ ->
           let rels = fst (splay_prod env none (type_of env c)) in
           let env = push_rels_assum rels env in
-          let eta_args = List.rev_map mkRel (interval 1 p) in
+          let eta_args = List.rev_map mkRel (List.interval 1 p) in
           extract_type env db 0 (lift p c) eta_args
 
 
@@ -356,9 +386,9 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
        When at toplevel of the monolithic case, we cannot do much
        (cf Vector and bug #2570) *)
     let equiv =
-      if lang () <> Ocaml ||
+      if lang () != Ocaml ||
 	 (not (modular ()) && at_toplevel (mind_modpath kn)) ||
-	 kn_ord (canonical_mind kn) (user_mind kn) = 0
+	 KerName.equal (canonical_mind kn) (user_mind kn)
       then
 	NoEquiv
       else
@@ -375,32 +405,34 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
     (* First pass: we store inductive signatures together with *)
     (* their type var list. *)
     let packets =
-      Array.map
-	(fun mip ->
-	   let b = snd (mind_arity mip) <> InProp in
-	   let ar = Inductive.type_of_inductive env (mib,mip) in
-	   let s,v = if b then type_sign_vl env ar else [],[] in
+      Array.mapi
+	(fun i mip ->
+	   let (ind,u), ctx = 
+	     Universes.fresh_inductive_instance env (kn,i) in
+	   let ar = Inductive.type_of_inductive env ((mib,mip),u) in
+	   let info = (fst (flag_of_type env ar) = Info) in
+	   let s,v = if info then type_sign_vl env ar else [],[] in
 	   let t = Array.make (Array.length mip.mind_nf_lc) [] in
 	   { ip_typename = mip.mind_typename;
 	     ip_consnames = mip.mind_consnames;
-	     ip_logical = (not b);
+	     ip_logical = not info;
 	     ip_sign = s;
 	     ip_vars = v;
-	     ip_types = t })
+	     ip_types = t }, u)
 	mib.mind_packets
     in
 
     add_ind kn mib
       {ind_kind = Standard;
        ind_nparams = npar;
-       ind_packets = packets;
+       ind_packets = Array.map fst packets;
        ind_equiv = equiv
       };
     (* Second pass: we extract constructors *)
     for i = 0 to mib.mind_ntypes - 1 do
-      let p = packets.(i) in
+      let p,u = packets.(i) in
       if not p.ip_logical then
-	let types = arities_of_constructors env (kn,i) in
+	let types = arities_of_constructors env ((kn,i),u) in
 	for j = 0 to Array.length types - 1 do
 	  let t = snd (decompose_prod_n npar types.(j)) in
 	  let prods,head = dest_prod epar t in
@@ -420,18 +452,18 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	let ip = (kn, 0) in
 	let r = IndRef ip in
 	if is_custom r then raise (I Standard);
-	if not mib.mind_finite then raise (I Coinductive);
-	if mib.mind_ntypes <> 1 then raise (I Standard);
-	let p = packets.(0) in
+	if mib.mind_finite == Decl_kinds.CoFinite then raise (I Coinductive);
+	if not (Int.equal mib.mind_ntypes 1) then raise (I Standard);
+	let p,u = packets.(0) in
 	if p.ip_logical then raise (I Standard);
-	if Array.length p.ip_types <> 1 then raise (I Standard);
+	if not (Int.equal (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 not (keep_singleton ()) &&
-	    List.length l = 1 && not (type_mem_kn kn (List.hd l))
+	    Int.equal (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);
+	if List.is_empty l then raise (I Standard);
+	if Option.is_empty mib.mind_record then raise (I Standard);
 	(* Now we're sure it's a record. *)
 	(* First, we find its field names. *)
 	let rec names_prod t = match kind_of_term t with
@@ -441,10 +473,10 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  | _ -> []
 	in
 	let field_names =
-	  list_skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
-	assert (List.length field_names = List.length typ);
+	  List.skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
+	assert (Int.equal (List.length field_names) (List.length typ));
 	let projs = ref Cset.empty in
-	let mp,d,_ = repr_mind kn in
+	let mp = MutInd.modpath kn in
 	let rec select_fields l typs = match l,typs with
 	  | [],[] -> []
 	  | _::l, typ::typs when isDummy (expand env typ) ->
@@ -452,9 +484,9 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	  | Anonymous::l, typ::typs ->
 	      None :: (select_fields l typs)
 	  | Name id::l, typ::typs ->
-	      let knp = make_con mp d (label_of_id id) in
+	      let knp = Constant.make2 mp (Label.of_id id) in
 	      (* Is it safe to use [id] for projections [foo.id] ? *)
-	      if List.for_all ((=) Keep) (type2signature env typ)
+	      if List.for_all ((==) Keep) (type2signature env typ)
 	      then projs := Cset.add knp !projs;
 	      Some (ConstRef knp) :: (select_fields l typs)
 	  | _ -> assert false
@@ -465,9 +497,10 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
 	(* If so, we use this information. *)
 	begin try
 	  let n = nb_default_params env
-            (Inductive.type_of_inductive env (mib,mip0))
+            (Inductive.type_of_inductive env ((mib,mip0),u))
 	  in
-	  let check_proj kn = if Cset.mem kn !projs then add_projection n kn in
+	  let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip
+          in
 	  List.iter (Option.iter check_proj) (lookup_projections ip)
 	with Not_found -> ()
 	end;
@@ -476,7 +509,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
     in
     let i = {ind_kind = ind_info;
 	     ind_nparams = npar;
-	     ind_packets = packets;
+	     ind_packets = Array.map fst packets;
 	     ind_equiv = equiv }
     in
     add_ind kn mib i;
@@ -495,7 +528,7 @@ and extract_type_cons env db dbmap c i =
   match kind_of_term (whd_betadeltaiota env none c) with
     | Prod (n,t,d) ->
 	let env' = push_rel_assum (n,t) env in
-	let db' = (try Intmap.find i dbmap with Not_found -> 0) :: db in
+	let db' = (try Int.Map.find i dbmap with Not_found -> 0) :: db in
 	let l = extract_type_cons env' db' dbmap d (i+1) in
 	(extract_type env db 0 t []) :: l
     | _ -> []
@@ -511,13 +544,14 @@ and mlt_env env r = match r with
 	   | _ -> None
        with Not_found ->
 	 let cb = Environ.lookup_constant kn env in
-	 let typ = Typeops.type_of_constant_type env cb.const_type in
+	 let typ = Typeops.type_of_constant_type env cb.const_type
+ (* FIXME not sure if we should instantiate univs here *) in
 	 match cb.const_body with
 	   | Undef _ | OpaqueDef _ -> None
 	   | Def l_body ->
 	       (match flag_of_type env typ with
 		  | Info,TypeScheme ->
-		      let body = Declarations.force l_body in
+		      let body = Mod_subst.force_constr l_body in
 		      let s,vl = type_sign_vl env typ in
 		      let db = db_from_sign s in
 		      let t = extract_type_scheme env db body (List.length s)
@@ -539,7 +573,7 @@ let record_constant_type env kn opt_typ =
     lookup_type kn
   with Not_found ->
     let typ = match opt_typ with
-      | None -> Typeops.type_of_constant env kn
+      | None -> Typeops.type_of_constant_type env (lookup_constant kn env).const_type
       | Some typ -> typ
     in let mlt = extract_type env [] 1 typ []
     in let schema = (type_maxvar mlt, mlt)
@@ -594,10 +628,12 @@ let rec extract_term env mle mlt c args =
 	with NotDefault d ->
 	  let mle' = Mlenv.push_std_type mle (Tdummy d) in
 	  ast_pop (extract_term env' mle' mlt c2 args'))
-    | Const kn ->
-	extract_cst_app env mle mlt kn args
-    | Construct cp ->
-	extract_cons_app env mle mlt cp args
+    | Const (kn,u) ->
+	extract_cst_app env mle mlt kn u args
+    | Construct (cp,u) ->
+	extract_cons_app env mle mlt cp u args
+    | Proj (p, c) ->
+        extract_cst_app env mle mlt (Projection.constant p) Univ.Instance.empty (c :: args)
     | Rel n ->
 	(* As soon as the expected [mlt] for the head is known, *)
 	(* we unify it with an fresh copy of the stored type of [Rel n]. *)
@@ -645,14 +681,15 @@ and make_mlargs env e s args typs =
 
 (*s Extraction of a constant applied to arguments. *)
 
-and extract_cst_app env mle mlt kn args =
+and extract_cst_app env mle mlt kn u args =
   (* First, the [ml_schema] of the constant, in expanded version. *)
   let nb,t = record_constant_type env kn None in
   let schema = nb, expand env t in
   (* Can we instantiate types variables for this constant ? *)
   (* In Ocaml, inside the definition of this constant, the answer is no. *)
   let instantiated =
-    if lang () = Ocaml && List.mem kn !current_fixpoints then var2var' (snd schema)
+    if lang () == Ocaml && List.mem_f Constant.equal kn !current_fixpoints
+    then var2var' (snd schema)
     else instantiation schema
   in
   (* Then the expected type of this constant. *)
@@ -674,14 +711,14 @@ and extract_cst_app env mle mlt kn args =
   (* The ml arguments, already expunged from known logical ones *)
   let mla = make_mlargs env mle s args metas in
   let mla =
-    if magic1 || lang () <> Ocaml then mla
+    if magic1 || lang () != Ocaml then mla
     else
       try
         (* for better optimisations later, we discard dependent args
            of projections and replace them by fake args that will be
            removed during final pretty-print. *)
-	let l,l' = list_chop (projection_arity (ConstRef kn)) mla in
-	if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
+	let l,l' = List.chop (projection_arity (ConstRef kn)) mla in
+	if not (List.is_empty l') then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
 	else mla
       with e when Errors.noncritical e -> mla
   in
@@ -689,7 +726,7 @@ and extract_cst_app env mle mlt kn args =
      one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left
      accordingly. *)
   let optdummy = match sign_kind s_full with
-    | UnsafeLogicalSig when lang () <> Haskell -> [MLdummy]
+    | UnsafeLogicalSig when lang () != Haskell -> [MLdummy]
     | _ -> []
   in
   (* Different situations depending of the number of arguments: *)
@@ -702,7 +739,7 @@ and extract_cst_app env mle mlt kn args =
     (* Partially applied function with some logical arg missing.
        We complete via eta and expunge logical args. *)
     let ls' = ls-la in
-    let s' = list_skipn la s in
+    let s' = List.skipn la s in
     let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
     let e = anonym_or_dummy_lams (mlapp head mla) s' in
     put_magic_if magic2 (remove_n_lams (List.length optdummy) e)
@@ -717,14 +754,14 @@ and extract_cst_app env mle mlt kn args =
    they are fixed, and thus are not used for the computation.
    \end{itemize} *)
 
-and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
+and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) u args =
   (* First, we build the type of the constructor, stored in small pieces. *)
   let mi = extract_ind env kn in
   let params_nb = mi.ind_nparams in
   let oi = mi.ind_packets.(i) in
   let nb_tvars = List.length oi.ip_vars
   and types = List.map (expand env) oi.ip_types.(j-1) in
-  let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvars) in
+  let list_tvar = List.map (fun i -> Tvar i) (List.interval 1 nb_tvars) in
   let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in
   let type_cons = instantiation (nb_tvars, type_cons) in
   (* Then, the usual variables [s], [ls], [la], ... *)
@@ -734,7 +771,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   let la = List.length args in
   assert (la <= ls + params_nb);
   let la' = max 0 (la - params_nb) in
-  let args' = list_lastn la' args in
+  let args' = List.lastn la' args in
   (* Now, we build the expected type of the constructor *)
   let metas = List.map new_meta args' in
   (* If stored and expected types differ, then magic! *)
@@ -742,7 +779,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
   let magic1 = needs_magic (type_cons, type_recomp (metas, a)) in
   let magic2 = needs_magic (a, mlt) in
   let head mla =
-    if mi.ind_kind = Singleton then
+    if mi.ind_kind == Singleton then
       put_magic_if magic1 (List.hd mla) (* assert (List.length mla = 1) *)
     else
       let typeargs = match snd (type_decomp type_cons) with
@@ -759,11 +796,11 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
       (dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la))
   else
     let mla = make_mlargs env mle s args' metas in
-    if la = ls + params_nb
+    if Int.equal la (ls + params_nb)
     then put_magic_if (magic2 && not magic1) (head mla)
     else (* [ params_nb <= la <= ls + params_nb ] *)
       let ls' = params_nb + ls - la in
-      let s' = list_lastn ls' s in
+      let s' = List.lastn ls' s in
       let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
       put_magic_if magic2 (anonym_or_dummy_lams (head mla) s')
 
@@ -772,22 +809,22 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
 and extract_case env mle ((kn,i) as ip,c,br) mlt =
   (* [br]: bodies of each branch (in functional form) *)
   (* [ni]: number of arguments without parameters in each branch *)
-  let ni = mis_constr_nargs_env env ip in
+  let ni = constructors_nrealargs_env env ip in
   let br_size = Array.length br in
-  assert (Array.length ni = br_size);
-  if br_size = 0 then begin
+  assert (Int.equal (Array.length ni) br_size);
+  if Int.equal br_size 0 then begin
     add_recursors env kn; (* May have passed unseen if logical ... *)
     MLexn "absurd case"
   end else
     (* [c] has an inductive type, and is not a type scheme type. *)
     let t = type_of env c in
     (* The only non-informative case: [c] is of sort [Prop] *)
-    if (sort_of env t) = InProp then
+    if (sort_of env t) == InProp then
       begin
 	add_recursors env kn; (* May have passed unseen if logical ... *)
 	(* Logical singleton case: *)
 	(* [match c with C i j k -> t] becomes [t'] *)
-	assert (br_size = 1);
+	assert (Int.equal br_size 1);
 	let s = iterate (fun l -> Kill Kother :: l) ni.(0) [] in
 	let mlt = iterate (fun t -> Tarr (Tdummy Kother, t)) ni.(0) mlt in
 	let e = extract_maybe_term env mle mlt br.(0) in
@@ -816,13 +853,13 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	let e' = handle_exn r (List.length s) (fun _ -> Anonymous) e in
 	(List.rev ids, Pusual r, e')
       in
-      if mi.ind_kind = Singleton then
+      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);
+	  assert (Int.equal br_size 1);
 	  let (ids,_,e') = extract_branch 0 in
-	  assert (List.length ids = 1);
+	  assert (Int.equal (List.length ids) 1);
 	  MLletin (tmp_id (List.hd ids),a,e')
 	end
       else
@@ -838,7 +875,7 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt =
   let metas = Array.map new_meta fi in
   metas.(i) <- mlt;
   let mle = Array.fold_left Mlenv.push_type mle metas in
-  let ei = array_map2 (extract_maybe_term env mle) metas ci in
+  let ei = Array.map2 (extract_maybe_term env mle) metas ci in
   MLfix (i, Array.map id_of_name fi, ei)
 
 (*S ML declarations. *)
@@ -846,14 +883,14 @@ and extract_fix env mle i (fi,ti,ci as recd) mlt =
 (* [decomp_lams_eta env c t] finds the number [n] of products in the type [t],
    and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *)
 
-let rec decomp_lams_eta_n n m env c t =
+let decomp_lams_eta_n n m env c t =
   let rels = fst (splay_prod_n env none n t) in
   let rels = List.map (fun (id,_,c) -> (id,c)) rels in
   let rels',c = decompose_lam c in
   let d = n - m in
   (* we'd better keep rels' as long as possible. *)
-  let rels = (list_firstn d rels) @ rels' in
-  let eta_args = List.rev_map mkRel (interval 1 d) in
+  let rels = (List.firstn d rels) @ rels' in
+  let eta_args = List.rev_map mkRel (List.interval 1 d) in
   rels, applist (lift d c,eta_args)
 
 (* Let's try to identify some situation where extracted code
@@ -864,7 +901,7 @@ let rec gentypvar_ok c = match kind_of_term c with
   | App (c,v) ->
       (* if all arguments are variables, these variables will
 	 disappear after extraction (see [empty_s] below) *)
-      array_for_all isRel v && gentypvar_ok c
+      Array.for_all isRel v && gentypvar_ok c
   | Cast (c,_,_) -> gentypvar_ok c
   | _ -> false
 
@@ -891,26 +928,26 @@ 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_chop m s in
-      if List.for_all ((=) Keep) s' &&
-	(lang () = Haskell || sign_kind s <> UnsafeLogicalSig)
+      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
       else decomp_lams_eta_n n m env body typ
   in
   (* Should we do one eta-expansion to avoid non-generalizable '_a ? *)
   let rels, c =
     let n = List.length rels in
-    let s,s' = list_chop 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)
-      && s' <> [] && type_maxvar t <> 0
+    let empty_s = (k == EmptySig || k == SafeLogicalSig) in
+    if lang () == Ocaml && empty_s && not (gentypvar_ok c)
+      && not (List.is_empty s') && not (Int.equal (type_maxvar t) 0)
     then decomp_lams_eta_n (n+1) n env body typ
     else rels,c
   in
   let n = List.length rels in
-  let s = list_firstn n s in
-  let l,l' = list_chop n l in
+  let s = List.firstn n s 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
@@ -948,7 +985,7 @@ let extract_fixpoint env vkn (fi,ti,ci) =
   (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *)
   let sub = List.rev_map mkConst kns in
   for i = 0 to n-1 do
-    if sort_of env ti.(i) <> InProp then begin
+    if sort_of env ti.(i) != InProp then begin
       let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in
       terms.(i) <- e;
       types.(i) <- t;
@@ -988,17 +1025,21 @@ let extract_constant env kn cb =
     | (Info,TypeScheme) ->
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_typ_ax ()
-	  | Def c -> mk_typ (force c)
+	  | Def c -> mk_typ (Mod_subst.force_constr c)
 	  | OpaqueDef c ->
 	    add_opaque r;
-	    if access_opaque () then mk_typ (force_opaque c) else mk_typ_ax ())
+	    if access_opaque () then
+              mk_typ (Opaqueproof.force_proof (Environ.opaque_tables env) c)
+            else mk_typ_ax ())
     | (Info,Default) ->
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_ax ()
-	  | Def c -> mk_def (force c)
+	  | Def c -> mk_def (Mod_subst.force_constr c)
 	  | OpaqueDef c ->
 	    add_opaque r;
-	    if access_opaque () then mk_def (force_opaque c) else mk_ax ())
+	    if access_opaque () then
+              mk_def (Opaqueproof.force_proof (Environ.opaque_tables env) c)
+            else mk_ax ())
 
 let extract_constant_spec env kn cb =
   let r = ConstRef kn in
@@ -1012,27 +1053,32 @@ let extract_constant_spec env kn cb =
 	  | 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)
+              let body = Mod_subst.force_constr body in
+	      let t = extract_type_scheme env db body (List.length s)
 	      in Stype (r, vl, Some t))
     | (Info, Default) ->
 	let t = snd (record_constant_type env kn (Some typ)) in
 	Sval (r, type_expunge env t)
 
-let extract_with_type env cb =
-  let typ = Typeops.type_of_constant_type env cb.const_type in
+let extract_with_type env c =
+  let typ = type_of env c in
   match flag_of_type env typ with
     | (Info, TypeScheme) ->
 	let s,vl = type_sign_vl env typ in
 	let db = db_from_sign 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
 
+let extract_constr env c =
+  reset_meta_count ();
+  let typ = type_of env c in
+  match flag_of_type env typ with
+    | (_,TypeScheme) -> MLdummy, Tdummy Ktype
+    | (Logic,_) -> MLdummy, Tdummy Kother
+    | (Info,Default) ->
+      let mlt = extract_type env [] 1 typ [] in
+      extract_term env Mlenv.empty mlt c [], mlt
 
 let extract_inductive env kn =
   let ind = extract_ind env kn in
@@ -1043,7 +1089,7 @@ let extract_inductive env kn =
       | [] -> []
       | t::l ->
 	  let l' = filter (succ i) l in
-	  if isDummy (expand env t) || List.mem i implicits then l'
+	  if isDummy (expand env t) || Int.List.mem i implicits then l'
 	  else t::l'
     in filter (1+ind.ind_nparams) l
   in
@@ -1058,9 +1104,9 @@ let logical_decl = function
   | Dterm (_,MLdummy,Tdummy _) -> true
   | Dtype (_,[],Tdummy _) -> true
   | Dfix (_,av,tv) ->
-      (array_for_all ((=) MLdummy) av) &&
-      (array_for_all isDummy tv)
-  | Dind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
+      (Array.for_all ((==) MLdummy) av) &&
+      (Array.for_all isDummy tv)
+  | Dind (_,i) -> Array.for_all (fun ip -> ip.ip_logical) i.ind_packets
   | _ -> false
 
 (*s Is a [ml_spec] logical ? *)
@@ -1068,5 +1114,5 @@ let logical_decl = function
 let logical_spec = function
   | Stype (_, [], Some (Tdummy _)) -> true
   | Sval (_,Tdummy _) -> true
-  | Sind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
+  | Sind (_,i) -> Array.for_all (fun ip -> ip.ip_logical) i.ind_packets
   | _ -> false
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index f10f3589..6bd2541b 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -12,20 +12,25 @@ open Names
 open Term
 open Declarations
 open Environ
-open Libnames
 open Miniml
 
 val extract_constant : env -> constant -> constant_body -> ml_decl
 
 val extract_constant_spec : env -> constant -> constant_body -> ml_spec
 
-val extract_with_type : env -> constant_body -> ( identifier list * ml_type ) option
+(** For extracting "module ... with ..." declaration *)
+
+val extract_with_type : env -> constr -> ( Id.t list * ml_type ) option
 
 val extract_fixpoint :
   env -> constant array -> (constr, types) prec_declaration -> ml_decl
 
 val extract_inductive : env -> mutual_inductive -> ml_ind
 
+(** For extraction compute *)
+
+val extract_constr : env -> constr -> ml_ast * ml_type
+
 (*s Is a [ml_decl] or a [ml_spec] logical ? *)
 
 val logical_decl : ml_decl -> bool
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index a2b6b14a..3caa558f 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -1,17 +1,15 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i camlp4deps: "parsing/grammar.cma" i*)
+(*i camlp4deps: "grammar/grammar.cma" i*)
 
 (* ML names *)
 
-open Vernacexpr
-open Pcoq
 open Genarg
 open Pp
 open Names
@@ -35,7 +33,7 @@ let pr_int_or_id _ _ _ = function
 ARGUMENT EXTEND int_or_id
   TYPED AS int_or_id
   PRINTED BY pr_int_or_id
-| [ preident(id) ] -> [ ArgId (id_of_string id) ]
+| [ preident(id) ] -> [ ArgId (Id.of_string id) ]
 | [ integer(i) ] -> [ ArgInt i ]
 END
 
@@ -53,7 +51,7 @@ END
 
 (* Extraction commands *)
 
-VERNAC COMMAND EXTEND Extraction
+VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY
 (* Extraction in the Coq toplevel *)
 | [ "Extraction" global(x) ] -> [ simple_extraction x ]
 | [ "Recursive" "Extraction" ne_global_list(l) ] -> [ full_extraction None l ]
@@ -63,85 +61,85 @@ VERNAC COMMAND EXTEND Extraction
   -> [ full_extraction (Some f) l ]
 END
 
-VERNAC COMMAND EXTEND SeparateExtraction
+VERNAC COMMAND EXTEND SeparateExtraction CLASSIFIED AS QUERY
 (* 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
+VERNAC COMMAND EXTEND ExtractionLibrary CLASSIFIED AS QUERY
 | [ "Extraction" "Library" ident(m) ]
   -> [ extraction_library false m ]
 END
 
-VERNAC COMMAND EXTEND RecursiveExtractionLibrary
+VERNAC COMMAND EXTEND RecursiveExtractionLibrary CLASSIFIED AS QUERY
 | [ "Recursive" "Extraction" "Library" ident(m) ]
   -> [ extraction_library true m ]
 END
 
 (* Target Language *)
-VERNAC COMMAND EXTEND ExtractionLanguage
+VERNAC COMMAND EXTEND ExtractionLanguage CLASSIFIED AS SIDEFF
 | [ "Extraction" "Language" language(l) ]
   -> [ extraction_language l ]
 END
 
-VERNAC COMMAND EXTEND ExtractionInline
+VERNAC COMMAND EXTEND ExtractionInline CLASSIFIED AS SIDEFF
 (* Custom inlining directives *)
 | [ "Extraction" "Inline" ne_global_list(l) ]
   -> [ extraction_inline true l ]
 END
 
-VERNAC COMMAND EXTEND ExtractionNoInline
+VERNAC COMMAND EXTEND ExtractionNoInline CLASSIFIED AS SIDEFF
 | [ "Extraction" "NoInline" ne_global_list(l) ]
   -> [ extraction_inline false l ]
 END
 
-VERNAC COMMAND EXTEND PrintExtractionInline
+VERNAC COMMAND EXTEND PrintExtractionInline CLASSIFIED AS QUERY
 | [ "Print" "Extraction" "Inline" ]
-  -> [ print_extraction_inline () ]
+  -> [ msg_info (print_extraction_inline ()) ]
 END
 
-VERNAC COMMAND EXTEND ResetExtractionInline
+VERNAC COMMAND EXTEND ResetExtractionInline CLASSIFIED AS SIDEFF
 | [ "Reset" "Extraction" "Inline" ]
   -> [ reset_extraction_inline () ]
 END
 
-VERNAC COMMAND EXTEND ExtractionImplicit
+VERNAC COMMAND EXTEND ExtractionImplicit CLASSIFIED AS SIDEFF
 (* Custom implicit arguments of some csts/inds/constructors *)
 | [ "Extraction" "Implicit" global(r) "[" int_or_id_list(l) "]" ]
   -> [ extraction_implicit r l ]
 END
 
-VERNAC COMMAND EXTEND ExtractionBlacklist
+VERNAC COMMAND EXTEND ExtractionBlacklist CLASSIFIED AS SIDEFF
 (* Force Extraction to not use some filenames *)
 | [ "Extraction" "Blacklist" ne_ident_list(l) ]
   -> [ extraction_blacklist l ]
 END
 
-VERNAC COMMAND EXTEND PrintExtractionBlacklist
+VERNAC COMMAND EXTEND PrintExtractionBlacklist CLASSIFIED AS QUERY
 | [ "Print" "Extraction" "Blacklist" ]
-  -> [ print_extraction_blacklist () ]
+  -> [ msg_info (print_extraction_blacklist ()) ]
 END
 
-VERNAC COMMAND EXTEND ResetExtractionBlacklist
+VERNAC COMMAND EXTEND ResetExtractionBlacklist CLASSIFIED AS SIDEFF
 | [ "Reset" "Extraction" "Blacklist" ]
   -> [ reset_extraction_blacklist () ]
 END
 
 
 (* Overriding of a Coq object by an ML one *)
-VERNAC COMMAND EXTEND ExtractionConstant
+VERNAC COMMAND EXTEND ExtractionConstant CLASSIFIED AS SIDEFF
 | [ "Extract" "Constant" global(x) string_list(idl) "=>" mlname(y) ]
   -> [ extract_constant_inline false x idl y ]
 END
 
-VERNAC COMMAND EXTEND ExtractionInlinedConstant
+VERNAC COMMAND EXTEND ExtractionInlinedConstant CLASSIFIED AS SIDEFF
 | [ "Extract" "Inlined" "Constant" global(x) "=>" mlname(y) ]
   -> [ extract_constant_inline true x [] y ]
 END
 
-VERNAC COMMAND EXTEND ExtractionInductive
+VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF
 | [ "Extract" "Inductive" global(x) "=>"
     mlname(id) "[" mlname_list(idl) "]" string_opt(o) ]
   -> [ extract_inductive x id idl o ]
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 4f9c6a71..5e08fef5 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,10 +9,11 @@
 (*s Production of Haskell syntax. *)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
-open Libnames
+open Globnames
 open Table
 open Miniml
 open Mlutil
@@ -20,38 +21,47 @@ open Common
 
 (*s Haskell renaming issues. *)
 
-let pr_lower_id id = str (String.uncapitalize (string_of_id id))
-let pr_upper_id id = str (String.capitalize (string_of_id id))
+let pr_lower_id id = str (String.uncapitalize (Id.to_string id))
+let pr_upper_id id = str (String.capitalize (Id.to_string id))
 
 let keywords =
-  List.fold_right (fun s -> Idset.add (id_of_string s))
+  List.fold_right (fun s -> Id.Set.add (Id.of_string s))
   [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else";
     "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance";
     "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_"; "__";
     "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ]
-  Idset.empty
+  Id.Set.empty
 
-let preamble mod_name used_modules usf =
+let pp_comment s = str "-- " ++ s ++ fnl ()
+let pp_bracket_comment s = str"{- " ++ hov 0 s ++ str" -}"
+
+let preamble mod_name comment used_modules usf =
   let pp_import mp = str ("import qualified "^ string_of_modfile mp ^"\n")
   in
   (if not usf.magic then mt ()
    else
-     str "{-# OPTIONS_GHC -cpp -fglasgow-exts #-}\n" ++
-     str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}\n\n")
+     str "{-# OPTIONS_GHC -cpp -XMagicHash #-}" ++ fnl () ++
+     str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}")
+  ++ fnl () ++ fnl ()
+  ++
+  (match comment with
+    | None -> mt ()
+    | Some com -> pp_bracket_comment com ++ fnl () ++ fnl ())
   ++
   str "module " ++ pr_upper_id mod_name ++ str " where" ++ fnl2 () ++
   str "import qualified Prelude" ++ fnl () ++
   prlist pp_import used_modules ++ fnl () ++
-  (if used_modules = [] then mt () else fnl ()) ++
+  (if List.is_empty used_modules then mt () else fnl ()) ++
   (if not usf.magic then mt ()
    else str "\
-\nunsafeCoerce :: a -> b\
 \n#ifdef __GLASGOW_HASKELL__\
 \nimport qualified GHC.Base\
+\nunsafeCoerce :: a -> b\
 \nunsafeCoerce = GHC.Base.unsafeCoerce#\
 \n#else\
 \n-- HUGS\
 \nimport qualified IOExts\
+\nunsafeCoerce :: a -> b\
 \nunsafeCoerce = IOExts.unsafeCoerce\
 \n#endif" ++ fnl2 ())
   ++
@@ -74,19 +84,15 @@ let pp_global k r =
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
 
-let kn_sig =
-  let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in
-  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 e when Errors.noncritical e -> (str "a" ++ int i))
+       with Failure _ -> (str "a" ++ int i))
     | Tglob (r,[]) -> pp_global Type r
     | Tglob (IndRef(kn,0),l)
-	when not (keep_singleton ()) && kn = mk_ind "Coq.Init.Specif" "sig" ->
+	when not (keep_singleton ()) && MutInd.equal kn (mk_ind "Coq.Init.Specif" "sig") ->
 	  pp_type true vl (List.hd l)
     | Tglob (r,l) ->
 	  pp_par par
@@ -140,7 +146,7 @@ let rec pp_expr par env args =
     | MLglob r ->
 	apply (pp_global Term r)
     | MLcons (_,r,a) as c ->
-        assert (args=[]);
+        assert (List.is_empty args);
         begin match a with
 	  | _ when is_native_char c -> pp_native_char c
 	  | [] -> pp_global Cons r
@@ -151,13 +157,13 @@ let rec pp_expr par env args =
 			prlist_with_sep spc (pp_expr true env []) a)
 	end
     | MLtuple l ->
-        assert (args=[]);
+        assert (List.is_empty 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
+	  if not (List.is_empty 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
@@ -185,7 +191,7 @@ let rec pp_expr par env args =
 
 and pp_cons_pat par r ppl =
   pp_par par
-    (pp_global Cons r ++ space_if (ppl<>[]) ++ prlist_with_sep spc identity ppl)
+    (pp_global Cons r ++ space_if (not (List.is_empty 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)
@@ -205,7 +211,7 @@ and pp_pat env pv =
   prvecti
     (fun i x ->
        pp_one_pat env pv.(i) ++
-       if i = Array.length pv - 1 then str "}" else
+       if Int.equal i (Array.length pv - 1) then str "}" else
 	 (str ";" ++ fnl ()))
     pv
 
@@ -218,7 +224,7 @@ and pp_fix par env i (ids,bl) args =
        (v 1 (str "let {" ++ fnl () ++
 	     prvect_with_sep (fun () -> str ";" ++ fnl ())
 	       (fun (fi,ti) -> pp_function env (pr_id fi) ti)
-	       (array_map2 (fun a b -> a,b) ids bl) ++
+	       (Array.map2 (fun a b -> a,b) ids bl) ++
 	     str "}") ++
         fnl () ++ str "in " ++ pp_apply (pr_id ids.(i)) false args))
 
@@ -231,8 +237,6 @@ and pp_function env f t =
 
 (*s Pretty-printing of inductive types declaration. *)
 
-let pp_comment s = str "-- " ++ s ++ fnl ()
-
 let pp_logical_ind packet =
   pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++
   pp_comment (str "with constructors : " ++
@@ -243,7 +247,7 @@ let pp_singleton kn packet =
   let l' = List.rev l in
   hov 2 (str "type " ++ pp_global Type (IndRef (kn,0)) ++ spc () ++
 	 prlist_with_sep spc pr_id l ++
-	 (if l <> [] then str " " else mt ()) ++ str "=" ++ spc () ++
+	 (if not (List.is_empty l) then str " " else mt ()) ++ str "=" ++ spc () ++
 	 pp_type false l' (List.hd packet.ip_types.(0)) ++ fnl () ++
 	 pp_comment (str "singleton inductive, whose constructor was " ++
 		     pr_id packet.ip_consnames.(0)))
@@ -258,10 +262,10 @@ let pp_one_ind ip pl cv =
       	       	prlist_with_sep
 		  (fun () -> (str " ")) (pp_type true pl) l))
   in
-  str (if Array.length cv = 0 then "type " else "data ") ++
+  str (if Array.is_empty cv then "type " else "data ") ++
   pp_global Type (IndRef ip) ++
   prlist_strict (fun id -> str " " ++ pr_lower_id id) pl ++ str " =" ++
-  if Array.length cv = 0 then str " () -- empty inductive"
+  if Array.is_empty cv then str " () -- empty inductive"
   else
     (fnl () ++ str " " ++
      v 0 (str "  " ++
@@ -286,7 +290,7 @@ let rec pp_ind first kn i ind =
 (*s Pretty-printing of a declaration. *)
 
 let pp_decl = function
-  | Dind (kn,i) when i.ind_kind = Singleton ->
+  | Dind (kn,i) when i.ind_kind == Singleton ->
       pp_singleton kn i.ind_packets.(0) ++ fnl ()
   | Dind (kn,i) -> hov 0 (pp_ind true kn 0 i)
   | Dtype (r, l, t) ->
@@ -299,7 +303,7 @@ let pp_decl = function
 	    prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s
 	  with Not_found ->
 	    prlist (fun id -> pr_id id ++ str " ") l ++
-	    if t = Taxiom then str "= () -- AXIOM TO BE REALIZED\n"
+	    if t == Taxiom then str "= () -- AXIOM TO BE REALIZED\n"
 	    else str "=" ++ spc () ++ pp_type false l t
 	in
 	hov 2 (str "type " ++ pp_global Type r ++ spc () ++ st) ++ fnl2 ()
@@ -310,7 +314,7 @@ let pp_decl = function
       prvecti
 	(fun i r ->
 	  let void = is_inline_custom r ||
-	    (not (is_custom r) && defs.(i) = MLexn "UNUSED")
+	    (not (is_custom r) && match defs.(i) with MLexn "UNUSED" -> true | _ -> false)
 	  in
 	  if void then mt ()
 	  else
@@ -359,7 +363,7 @@ let haskell_descr = {
   preamble = preamble;
   pp_struct = pp_struct;
   sig_suffix = None;
-  sig_preamble = (fun _ _ _ -> mt ());
+  sig_preamble = (fun _ _ _ _ -> mt ());
   pp_sig = (fun _ -> mt ());
   pp_decl = pp_decl;
 }
diff --git a/plugins/extraction/haskell.mli b/plugins/extraction/haskell.mli
index b00fc42f..99559bce 100644
--- a/plugins/extraction/haskell.mli
+++ b/plugins/extraction/haskell.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index fbb1c116..1e491d36 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,9 +9,8 @@
 (*s Target language for extraction: a core ML called MiniML. *)
 
 open Pp
-open Util
 open Names
-open Libnames
+open Globnames
 
 (* The [signature] type is used to know how many arguments a CIC
    object expects, and what these arguments will become in the ML
@@ -66,11 +65,11 @@ type inductive_kind =
 *)
 
 type ml_ind_packet = {
-  ip_typename : identifier;
-  ip_consnames : identifier array;
+  ip_typename : Id.t;
+  ip_consnames : Id.t array;
   ip_logical : bool;
   ip_sign : signature;
-  ip_vars : identifier list;
+  ip_vars : Id.t list;
   ip_types : (ml_type list) array
 }
 
@@ -92,8 +91,8 @@ type ml_ind = {
 
 type ml_ident =
   | Dummy
-  | Id of identifier
-  | Tmp of identifier
+  | Id of Id.t
+  | Tmp of Id.t
 
 (** We now store some typing information on constructors
     and cases to avoid type-unsafe optimisations. This will be
@@ -117,7 +116,7 @@ and ml_ast =
   | 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
+  | MLfix    of int * Id.t array * ml_ast array
   | MLexn    of string
   | MLdummy
   | MLaxiom
@@ -134,13 +133,13 @@ and ml_pattern =
 
 type ml_decl =
   | Dind  of mutual_inductive * ml_ind
-  | Dtype of global_reference * identifier list * ml_type
+  | Dtype of global_reference * Id.t 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 mutual_inductive * ml_ind
-  | Stype of global_reference * identifier list * ml_type option
+  | Stype of global_reference * Id.t list * ml_type option
   | Sval  of global_reference * ml_type
 
 type ml_specif =
@@ -150,15 +149,15 @@ type ml_specif =
 
 and ml_module_type =
   | MTident of module_path
-  | MTfunsig of mod_bound_id * ml_module_type * ml_module_type
+  | MTfunsig of MBId.t * ml_module_type * ml_module_type
   | MTsig of module_path * ml_module_sig
   | MTwith of ml_module_type * ml_with_declaration
 
 and ml_with_declaration =
-  | ML_With_type of identifier list * identifier list * ml_type
-  | ML_With_module of identifier list * module_path
+  | ML_With_type of Id.t list * Id.t list * ml_type
+  | ML_With_module of Id.t list * module_path
 
-and ml_module_sig = (label * ml_specif) list
+and ml_module_sig = (Label.t * ml_specif) list
 
 type ml_structure_elem =
   | SEdecl of ml_decl
@@ -167,11 +166,11 @@ type ml_structure_elem =
 
 and ml_module_expr =
   | MEident of module_path
-  | MEfunctor of mod_bound_id * ml_module_type * ml_module_expr
+  | MEfunctor of MBId.t * ml_module_type * ml_module_expr
   | MEstruct of module_path * ml_module_structure
   | MEapply of ml_module_expr * ml_module_expr
 
-and ml_module_structure = (label * ml_structure_elem) list
+and ml_module_structure = (Label.t * ml_structure_elem) list
 
 and ml_module =
     { ml_mod_expr : ml_module_expr;
@@ -184,6 +183,8 @@ type ml_structure = (module_path * ml_module_structure) list
 
 type ml_signature = (module_path * ml_module_sig) list
 
+type ml_flat_structure = ml_structure_elem list
+
 type unsafe_needs = {
   mldummy : bool;
   tdummy : bool;
@@ -192,16 +193,22 @@ type unsafe_needs = {
 }
 
 type language_descr = {
-  keywords : Idset.t;
+  keywords : Id.Set.t;
 
   (* Concerning the source file *)
   file_suffix : string;
-  preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds;
+  (* the second argument is a comment to add to the preamble *)
+  preamble :
+    Id.t -> std_ppcmds option -> module_path list -> unsafe_needs ->
+    std_ppcmds;
   pp_struct : ml_structure -> std_ppcmds;
 
   (* Concerning a possible interface file *)
   sig_suffix : string option;
-  sig_preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds;
+  (* the second argument is a comment to add to the preamble *)
+  sig_preamble :
+    Id.t -> std_ppcmds option -> module_path list -> unsafe_needs ->
+    std_ppcmds;
   pp_sig : ml_signature -> std_ppcmds;
 
   (* for an isolated declaration print *)
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 1462d3e7..9fdb0205 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1,17 +1,16 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 (*i*)
-open Pp
 open Util
 open Names
 open Libnames
-open Nametab
+open Globnames
 open Table
 open Miniml
 (*i*)
@@ -23,14 +22,14 @@ exception Impossible
 
 (*S Names operations. *)
 
-let anonymous_name = id_of_string "x"
-let dummy_name = id_of_string "_"
+let anonymous_name = Id.of_string "x"
+let dummy_name = Id.of_string "_"
 
 let anonymous = Id anonymous_name
 
 let id_of_name = function
   | Anonymous -> anonymous_name
-  | Name id when id = dummy_name -> anonymous_name
+  | Name id when Id.equal id dummy_name -> anonymous_name
   | Name id -> id
 
 let id_of_mlid = function
@@ -54,6 +53,22 @@ let new_meta _ =
   incr meta_count;
   Tmeta {id = !meta_count; contents = None}
 
+let rec eq_ml_type t1 t2 = match t1, t2 with
+| Tarr (tl1, tr1), Tarr (tl2, tr2) ->
+  eq_ml_type tl1 tl2 && eq_ml_type tr1 tr2
+| Tglob (gr1, t1), Tglob (gr2, t2) ->
+  eq_gr gr1 gr2 && List.equal eq_ml_type t1 t2
+| Tvar i1, Tvar i2 -> Int.equal i1 i2
+| Tvar' i1, Tvar' i2 -> Int.equal i1 i2
+| Tmeta m1, Tmeta m2 -> eq_ml_meta m1 m2
+| Tdummy k1, Tdummy k2 -> k1 == k2
+| Tunknown, Tunknown -> true
+| Taxiom, Taxiom -> true
+| _ -> false
+
+and eq_ml_meta m1 m2 =
+ Int.equal m1.id m2.id && Option.equal eq_ml_type m1.contents m2.contents
+
 (* Simultaneous substitution of [[Tvar 1; ... ; Tvar n]] by [l] in a ML type. *)
 
 let type_subst_list l t =
@@ -86,7 +101,7 @@ let instantiation (nb,t) = type_subst_vect (Array.init nb new_meta) t
 
 let rec type_occurs alpha t =
   match t with
-  | Tmeta {id=beta; contents=None} -> alpha = beta
+  | Tmeta {id=beta; contents=None} -> Int.equal alpha beta
   | Tmeta {contents=Some u} -> type_occurs alpha u
   | Tarr (t1, t2) -> type_occurs alpha t1 || type_occurs alpha t2
   | Tglob (r,l) -> List.exists (type_occurs alpha) l
@@ -95,7 +110,7 @@ let rec type_occurs alpha t =
 (*s Most General Unificator *)
 
 let rec mgu = function
-  | Tmeta m, Tmeta m' when m.id = m'.id -> ()
+  | Tmeta m, Tmeta m' when Int.equal m.id m'.id -> ()
   | Tmeta m, t | t, Tmeta m ->
     (match m.contents with
       | Some u -> mgu (u, t)
@@ -103,21 +118,24 @@ let rec mgu = function
       | None -> m.contents <- Some t)
   | Tarr(a, b), Tarr(a', b') ->
       mgu (a, a'); mgu (b, b')
-  | Tglob (r,l), Tglob (r',l') when r = r' ->
+  | Tglob (r,l), Tglob (r',l') when Globnames.eq_gr r r' ->
        List.iter mgu (List.combine l l')
-  | (Tdummy _, _ | _, Tdummy _) when lang() = Haskell -> ()
+  | (Tdummy _, _ | _, Tdummy _) when lang() == Haskell -> ()
   | Tdummy _, Tdummy _ -> ()
-  | t, u when t = u -> () (* for Tvar, Tvar', Tunknown, Taxiom *)
+  | Tvar i, Tvar j when Int.equal i j -> ()
+  | Tvar' i, Tvar' j when  Int.equal i j -> ()
+  | Tunknown, Tunknown -> ()
+  | Taxiom, Taxiom -> ()
   | _ -> raise Impossible
 
 let needs_magic p = try mgu p; false with Impossible -> true
 
-let put_magic_if b a = if b && lang () <> Scheme then MLmagic a else a
+let put_magic_if b a = if b && lang () != Scheme then MLmagic a else a
 
-let put_magic p a = if needs_magic p && lang () <> Scheme then MLmagic a else a
+let put_magic p a = if needs_magic p && lang () != Scheme then MLmagic a else a
 
 let generalizable a =
-  lang () <> Ocaml ||
+  lang () != Ocaml ||
     match a with
       | MLapp _ -> false
       | _ -> true (* TODO, this is just an approximation for the moment *)
@@ -148,7 +166,7 @@ module Mlenv = struct
   (* [find_free] finds the free meta in a type. *)
 
   let rec find_free set = function
-    | Tmeta m when m.contents = None -> Metaset.add m set
+    | Tmeta m when Option.is_empty m.contents -> Metaset.add m set
     | Tmeta {contents = Some t} -> find_free set t
     | Tarr (a,b) -> find_free (find_free set a) b
     | Tglob (_,l) -> List.fold_left find_free set l
@@ -172,12 +190,12 @@ module Mlenv = struct
 
   let generalization mle t =
     let c = ref 0 in
-    let map = ref (Intmap.empty : int Intmap.t) in
-    let add_new i = incr c; map := Intmap.add i !c !map; !c in
+    let map = ref (Int.Map.empty : int Int.Map.t) in
+    let add_new i = incr c; map := Int.Map.add i !c !map; !c in
     let rec meta2var t = match t with
       | Tmeta {contents=Some u} -> meta2var u
       | Tmeta ({id=i} as m) ->
-	  (try Tvar (Intmap.find i !map)
+	  (try Tvar (Int.Map.find i !map)
 	   with Not_found ->
 	     if Metaset.mem m mle.free then t
 	     else Tvar (add_new i))
@@ -225,21 +243,6 @@ let type_maxvar t =
     | _ -> n
   in parse 0 t
 
-(*s What are the type variables occurring in [t]. *)
-
-let intset_union_map_list f l =
-  List.fold_left (fun s t -> Intset.union s (f t)) Intset.empty l
-
-let intset_union_map_array f a =
-  Array.fold_left (fun s t -> Intset.union s (f t)) Intset.empty a
-
-let rec type_listvar = function
-  | Tmeta {contents = Some t} -> type_listvar t
-  | Tvar i | Tvar' i -> Intset.singleton i
-  | Tarr (a,b) -> Intset.union (type_listvar a) (type_listvar b)
-  | Tglob (_,l) -> intset_union_map_list type_listvar l
-  | _ -> Intset.empty
-
 (*s From [a -> b -> c] to [[a;b],c]. *)
 
 let rec type_decomp = function
@@ -283,13 +286,13 @@ let type_simpl = type_expand (fun _ -> None)
 (*s Generating a signature from a ML type. *)
 
 let type_to_sign env t = match type_expand env t with
-  | Tdummy d -> Kill d
+  | Tdummy d when not (conservative_types ()) -> Kill d
   | _ -> Keep
 
 let type_to_signature env t =
   let rec f = function
     | Tmeta {contents = Some t} -> f t
-    | Tarr (Tdummy d, b) -> Kill d :: f b
+    | Tarr (Tdummy d, b) when not (conservative_types ())  -> Kill d :: f b
     | Tarr (_, b) -> Keep :: f b
     | _ -> []
   in f (type_expand env t)
@@ -318,7 +321,7 @@ let rec sign_kind = function
 	| NonLogicalSig -> NonLogicalSig
 	| UnsafeLogicalSig -> UnsafeLogicalSig
 	| SafeLogicalSig | EmptySig ->
-	    if k = Kother then UnsafeLogicalSig else SafeLogicalSig
+	    if k == Kother then UnsafeLogicalSig else SafeLogicalSig
 
 (* Removing the final [Keep] in a signature *)
 
@@ -326,17 +329,17 @@ let rec sign_no_final_keeps = function
   | [] -> []
   | k :: s ->
       let s' = k :: sign_no_final_keeps s in
-      if s' = [Keep] then [] else s'
+      match s' with [Keep] -> [] | _ -> s'
 
 (*s Removing [Tdummy] from the top level of a ML type. *)
 
 let type_expunge_from_sign env s t =
   let rec expunge s t =
-    if s = [] then t else match t with
+    if List.is_empty s then t else match t with
       | Tmeta {contents = Some t} -> expunge s t
       | Tarr (a,b) ->
 	  let t = expunge (List.tl s) b in
-	  if List.hd s = Keep then Tarr (a, t) else t
+	  if List.hd s == Keep then Tarr (a, t) else t
       | Tglob (r,l) ->
 	  (match env r with
 	     | Some mlt -> expunge s (type_subst_list l mlt)
@@ -344,7 +347,7 @@ let type_expunge_from_sign env s t =
       | _ -> assert false
   in
   let t = expunge (sign_no_final_keeps s) t in
-  if lang () <> Haskell && sign_kind s = UnsafeLogicalSig then
+  if lang () != Haskell && sign_kind s == UnsafeLogicalSig then
     Tarr (Tdummy Kother, t)
   else t
 
@@ -353,7 +356,55 @@ let type_expunge env t =
 
 (*S Generic functions over ML ast terms. *)
 
-let mlapp f a = if a = [] then f else MLapp (f,a)
+let mlapp f a = if List.is_empty a then f else MLapp (f,a)
+
+(** Equality *)
+
+let eq_ml_ident i1 i2 = match i1, i2 with
+| Dummy, Dummy -> true
+| Id id1, Id id2 -> Id.equal id1 id2
+| Tmp id1, Tmp id2 -> Id.equal id1 id2
+| _ -> false
+
+let rec eq_ml_ast t1 t2 = match t1, t2 with
+| MLrel i1, MLrel i2 ->
+  Int.equal i1 i2
+| MLapp (f1, t1), MLapp (f2, t2) ->
+  eq_ml_ast f1 f2 && List.equal eq_ml_ast t1 t2
+| MLlam (na1, t1), MLlam (na2, t2) ->
+  eq_ml_ident na1 na2 && eq_ml_ast t1 t2
+| MLletin (na1, c1, t1), MLletin (na2, c2, t2) ->
+  eq_ml_ident na1 na2 && eq_ml_ast c1 c2 && eq_ml_ast t1 t2
+| MLglob gr1, MLglob gr2 -> eq_gr gr1 gr2
+| MLcons (t1, gr1, c1), MLcons (t2, gr2, c2) ->
+  eq_ml_type t1 t2 && eq_gr gr1 gr2 && List.equal eq_ml_ast c1 c2
+| MLtuple t1, MLtuple t2 ->
+  List.equal eq_ml_ast t1 t2
+| MLcase (t1, c1, p1), MLcase (t2, c2, p2) ->
+  eq_ml_type t1 t2 && eq_ml_ast c1 c2 && Array.equal eq_ml_branch p1 p2
+| MLfix (i1, id1, t1), MLfix (i2, id2, t2) ->
+  Int.equal i1 i2 && Array.equal Id.equal id1 id2 && Array.equal eq_ml_ast t1 t2
+| MLexn e1, MLexn e2 -> String.equal e1 e2
+| MLdummy, MLdummy -> true
+| MLaxiom, MLaxiom -> true
+| MLmagic t1, MLmagic t2 -> eq_ml_ast t1 t2
+| _ -> false
+
+and eq_ml_pattern p1 p2 = match p1, p2 with
+| Pcons (gr1, p1), Pcons (gr2, p2) ->
+  eq_gr gr1 gr2 && List.equal eq_ml_pattern p1 p2
+| Ptuple p1, Ptuple p2 ->
+  List.equal eq_ml_pattern p1 p2
+| Prel i1, Prel i2 ->
+  Int.equal i1 i2
+| Pwild, Pwild -> true
+| Pusual gr1, Pusual gr2 -> eq_gr gr1 gr2
+| _ -> false
+
+and eq_ml_branch (id1, p1, t1) (id2, p2, t2) =
+  List.equal eq_ml_ident id1 id2 &&
+  eq_ml_pattern p1 p2 &&
+  eq_ml_ast t1 t2
 
 (*s [ast_iter_rel f t] applies [f] on every [MLrel] in t. It takes care
    of the number of bingings crossed before reaching the [MLrel]. *)
@@ -428,7 +479,7 @@ let ast_iter f = function
 
 let ast_occurs k t =
   try
-    ast_iter_rel (fun i -> if i = k then raise Found) t; false
+    ast_iter_rel (fun i -> if Int.equal i k then raise Found) t; false
   with Found -> true
 
 (*s [occurs_itvl k k' t] returns [true] if there is a [(Rel i)]
@@ -444,7 +495,7 @@ let ast_occurs_itvl k k' t =
 
 let nb_occur_match =
   let rec nb k = function
-    | MLrel i -> if i = k then 1 else 0
+    | MLrel i -> if Int.equal i k then 1 else 0
     | MLcase(_,a,v) ->
         (nb k a) +
 	Array.fold_left
@@ -466,7 +517,7 @@ let ast_lift k t =
   let rec liftrec n = function
     | MLrel i as a -> if i-n < 1 then a else MLrel (i+k)
     | a -> ast_map_lift liftrec n a
-  in if k = 0 then t else liftrec 0 t
+  in if Int.equal k 0 then t else liftrec 0 t
 
 let ast_pop t = ast_lift (-1) t
 
@@ -490,7 +541,7 @@ let ast_subst e =
   let rec subst n = function
     | MLrel i as a ->
 	let i' = i-n in
-	if i'=1 then ast_lift n e
+	if Int.equal i' 1 then ast_lift n e
 	else if i'<1 then a
 	else MLrel (i-1)
     | a -> ast_map_lift subst n a
@@ -525,17 +576,18 @@ let has_deep_pattern br =
     | Pcons (_,l) | Ptuple l -> not (List.for_all is_basic_pattern l)
     | Pusual _ | Prel _ | Pwild -> false
   in
-  array_exists (function (_,pat,_) -> deep pat) br
+  Array.exists (function (_,pat,_) -> deep pat) br
 
 let is_regular_match br =
-  if Array.length br = 0 then false (* empty match becomes MLexn *)
+  if Array.is_empty br 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))
+            let is_rel i = function Prel j -> Int.equal i j | _ -> false in
+	    if not (List.for_all_i is_rel 1 (List.rev l))
 	    then raise Impossible;
 	    r
 	  | _ -> raise Impossible
@@ -544,7 +596,11 @@ let is_regular_match br =
 	| ConstructRef (ind,_) -> ind
 	| _ -> raise Impossible
       in
-      array_for_all_i (fun i tr -> get_r tr = ConstructRef (ind,i+1)) 0 br
+      let is_ref i tr = match get_r tr with
+      | ConstructRef (ind', j) -> eq_ind ind ind' && Int.equal j (i + 1)
+      | _ -> false
+      in
+      Array.for_all_i is_ref 0 br
     with Impossible -> false
 
 (*S Operations concerning lambdas. *)
@@ -562,7 +618,7 @@ let collect_lams =
 
 let collect_n_lams =
   let rec collect acc n t =
-    if n = 0 then acc,t
+    if Int.equal n 0 then acc,t
     else match t with
       | MLlam(id,t) -> collect (id::acc) (n-1) t
       | _ -> assert false
@@ -571,7 +627,7 @@ let collect_n_lams =
 (*s [remove_n_lams] just removes some [MLlam]. *)
 
 let rec remove_n_lams n t =
-  if n = 0 then t
+  if Int.equal n 0 then t
   else match t with
       | MLlam(_,t) -> remove_n_lams (n-1) t
       | _ -> assert false
@@ -609,7 +665,7 @@ let rec anonym_or_dummy_lams a = function
 (*s The following function creates [MLrel n;...;MLrel 1] *)
 
 let rec eta_args n =
-  if n = 0 then [] else (MLrel n)::(eta_args (pred n))
+  if Int.equal n 0 then [] else (MLrel n)::(eta_args (pred n))
 
 (*s Same, but filtered by a signature. *)
 
@@ -621,25 +677,26 @@ let rec eta_args_sign n = function
 (*s This one tests [MLrel (n+k); ... ;MLrel (1+k)] *)
 
 let rec test_eta_args_lift k n = function
-  | [] -> n=0
-  | a :: q -> (a = (MLrel (k+n))) && (test_eta_args_lift k (pred n) q)
+  | [] -> Int.equal n 0
+  | MLrel m :: q -> Int.equal (k+n) m && (test_eta_args_lift k (pred n) q)
+  | _ -> false
 
 (*s Computes an eta-reduction. *)
 
 let eta_red e =
   let ids,t = collect_lams e in
   let n = List.length ids in
-  if n = 0 then e
+  if Int.equal n 0 then e
   else match t with
     | MLapp (f,a) ->
 	let m = List.length a in
 	let ids,body,args =
-	  if m = n then
+	  if Int.equal m n then
 	    [], f, a
 	  else if m < n then
-	    list_skipn m ids, f, a
+	    List.skipn m ids, f, a
 	  else (* m > n *)
-	    let a1,a2 = list_chop (m-n) a in
+	    let a1,a2 = List.chop (m-n) a in
 	    [], MLapp (f,a1), a2
 	in
 	let p = List.length args in
@@ -715,7 +772,7 @@ let branch_as_fun typ (l,p,c) =
 	if i'<1 then c
 	else if i'>nargs then MLrel (i-nargs+1)
 	else raise Impossible
-    | MLcons _ as cons' when cons' = ast_lift n cons -> MLrel (n+1)
+    | MLcons _ as cons' when eq_ml_ast cons' (ast_lift n cons) -> MLrel (n+1)
     | a -> ast_map_lift genrec n a
   in genrec 0 c
 
@@ -739,27 +796,33 @@ let branch_as_cst (l,_,c) =
    When searching for the best factorisation below, we'll try both.
 *)
 
-(* The following structure allows to record which element occurred
+(* The following structure allows recording which element occurred
    at what position, and then finally return the most frequent
    element and its positions. *)
 
 let census_add, census_max, census_clean =
-  let h = Hashtbl.create 13 in
-  let clear () = Hashtbl.clear h in
-  let add e i =
-    let s = try Hashtbl.find h e with Not_found -> Intset.empty in
-    Hashtbl.replace h e (Intset.add i s)
+  let h = ref [] in
+  let clearf () = h := [] in
+  let rec add k v = function
+  | [] -> raise Not_found
+  | (k', s) as p :: l ->
+    if eq_ml_ast k k' then (k', Int.Set.add v s) :: l
+    else p :: add k v l
+  in
+  let addf k i =
+    try h := add k i !h
+    with Not_found -> h := (k, Int.Set.singleton i) :: !h
   in
-  let max e0 =
-    let len = ref 0 and lst = ref Intset.empty and elm = ref e0 in
-    Hashtbl.iter
-      (fun e s ->
-	 let n = Intset.cardinal s in
+  let maxf k =
+    let len = ref 0 and lst = ref Int.Set.empty and elm = ref k in
+    List.iter
+      (fun (e, s) ->
+	 let n = Int.Set.cardinal s in
 	 if n > !len then begin len := n; lst := s; elm := e end)
-      h;
+      !h;
     (!elm,!lst)
   in
-  (add,max,clear)
+  (addf,maxf,clearf)
 
 (* [factor_branches] return the longest possible list of branches
    that have the same factorization, either as a function or as a
@@ -771,7 +834,7 @@ let is_opt_pat (_,p,_) = match p with
   | _ -> false
 
 let factor_branches o typ br =
-  if array_exists is_opt_pat br then None (* already optimized *)
+  if Array.exists is_opt_pat br then None (* already optimized *)
   else begin
     census_clean ();
     for i = 0 to Array.length br - 1 do
@@ -782,8 +845,8 @@ let factor_branches o typ br =
     done;
     let br_factor, br_set = census_max MLdummy in
     census_clean ();
-    let n = Intset.cardinal br_set in
-    if n = 0 then None
+    let n = Int.Set.cardinal br_set in
+    if Int.equal n 0 then None
     else if Array.length br >= 2 && n < 2 then None
     else Some (br_factor, br_set)
   end
@@ -794,17 +857,17 @@ let rec merge_ids ids ids' = match ids,ids' with
   | [],l -> l
   | l,[] -> l
   | i::ids, i'::ids' ->
-      (if i = Dummy then i' else i) :: (merge_ids ids ids')
+      (if i == Dummy then i' else i) :: (merge_ids ids ids')
 
 let is_exn = function MLexn _ -> true | _ -> false
 
-let rec permut_case_fun br acc =
+let permut_case_fun br acc =
   let nb = ref max_int in
   Array.iter (fun (_,_,t) ->
 		let ids, c = collect_lams t in
 		let n = List.length ids in
 		if (n < !nb) && (not (is_exn c)) then nb := n) br;
-  if !nb = max_int || !nb = 0 then ([],br)
+  if Int.equal !nb  max_int || Int.equal !nb 0 then ([],br)
   else begin
     let br = Array.copy br in
     let ids = ref [] in
@@ -837,16 +900,16 @@ 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' | Pcons (r',_) when not (Globnames.eq_gr 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 ->
+    | Prel 1 when Int.equal (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
+    | Pwild when List.is_empty ids -> ast_lift lift c
     | _ -> raise Impossible (* TODO: handle some more cases *)
 
 (* [iota_gen] is an extension of [iota_red] where we allow to
@@ -872,15 +935,11 @@ let is_imm_apply = function MLapp (MLrel 1, _) -> true | _ -> false
     Unfolding them leads to more natural code (and more dummy removal) *)
 
 let is_program_branch = function
-  | Id id ->
-    let s = string_of_id id in
-    let br = "program_branch_" in
-    let n = String.length br in
-    (try
-       ignore (int_of_string (String.sub s n (String.length s - n)));
-       String.sub s 0 n = br
-     with e when Errors.noncritical e -> false)
   | Tmp _ | Dummy -> false
+  | Id id ->
+    let s = Id.to_string id in
+    try Scanf.sscanf s "program_branch_%d%!" (fun _ -> true)
+    with Scanf.Scan_failure _ | End_of_file -> false
 
 let expand_linear_let o id e =
    o.opt_lin_let || is_tmp id || is_program_branch id || is_imm_apply e
@@ -901,7 +960,7 @@ let rec simpl o = function
       if
 	(is_atomic c) || (is_atomic e) ||
 	(let n = nb_occur_match e in
-	 (n = 0 || (n=1 && expand_linear_let o id e)))
+	 (Int.equal n 0 || (Int.equal n 1 && expand_linear_let o id e)))
       then
 	simpl o (ast_subst c e)
       else
@@ -954,14 +1013,14 @@ and simpl_case o typ br e =
     (* 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
+    if not (Int.equal n 0) then
       simpl o (named_lams ids (MLcase (typ, ast_lift n e, br)))
     else
       (* Can we merge several branches as the same constant or function ? *)
-      if lang() = Scheme || is_custom_match br
+      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 ->
+	| Some (f,ints) when Int.equal (Int.Set.cardinal ints) (Array.length br) ->
 	  (* If all branches have been factorized, we remove the match *)
 	  simpl o (MLletin (Tmp anonymous_name, e, f))
 	| Some (f,ints) ->
@@ -970,7 +1029,7 @@ and simpl_case o typ br e =
 	    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 = List.filteri (fun i _ -> not (Int.Set.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)
@@ -996,9 +1055,9 @@ let rec select_via_bl l args = match l,args with
 
 let kill_some_lams bl (ids,c) =
   let n = List.length bl in
-  let n' = List.fold_left (fun n b -> if b=Keep then (n+1) else n) 0 bl in
-  if n = n' then ids,c
-  else if n' = 0 then [],ast_lift (-n) c
+  let n' = List.fold_left (fun n b -> if b == Keep then (n+1) else n) 0 bl in
+  if Int.equal n n' then ids,c
+  else if Int.equal n' 0 then [],ast_lift (-n) c
   else begin
     let v = Array.make n None in
     let rec parse_ids i j = function
@@ -1016,15 +1075,15 @@ let kill_some_lams bl (ids,c) =
 let kill_dummy_lams c =
   let ids,c = collect_lams c in
   let bl = List.map sign_of_id ids in
-  if not (List.mem Keep bl) then raise Impossible;
+  if not (List.memq Keep bl) then raise Impossible;
   let rec fst_kill n = function
     | [] -> raise Impossible
     | Kill _ :: bl -> n
     | Keep :: bl -> fst_kill (n+1) bl
   in
   let skip = max 0 ((fst_kill 0 bl) - 1) in
-  let ids_skip, ids = list_chop skip ids in
-  let _, bl = list_chop skip bl in
+  let ids_skip, ids = List.chop skip ids in
+  let _, bl = List.chop skip bl in
   let c = named_lams ids_skip c in
   let ids',c = kill_some_lams bl (ids,c) in
   ids, named_lams ids' c
@@ -1052,7 +1111,7 @@ let case_expunge s e =
   let m = List.length s in
   let n = nb_lams e in
   let p = if m <= n then collect_n_lams m e
-  else eta_expansion_sign (list_skipn n s) (collect_lams e) in
+  else eta_expansion_sign (List.skipn n s) (collect_lams e) in
   kill_some_lams (List.rev s) p
 
 (*s [term_expunge] takes a function [fun idn ... id1 -> c]
@@ -1061,10 +1120,10 @@ let case_expunge s e =
   if all lambdas are logical dummy and the target language is strict. *)
 
 let term_expunge s (ids,c) =
-  if s = [] then c
+  if List.is_empty s then c
   else
     let ids,c = kill_some_lams (List.rev s) (ids,c) in
-    if ids = [] && lang () <> Haskell && List.mem (Kill Kother) s then
+    if List.is_empty ids && lang () != Haskell && List.mem (Kill Kother) s then
       MLlam (Dummy, ast_lift 1 c)
     else named_lams ids c
 
@@ -1076,7 +1135,7 @@ let kill_dummy_args ids r t =
   let m = List.length ids in
   let bl = List.rev_map sign_of_id ids in
   let rec found n = function
-    | MLrel r' when r' = r + n -> true
+    | MLrel r' when Int.equal r' (r + n) -> true
     | MLmagic e -> found n e
     | _ -> false
   in
@@ -1086,7 +1145,7 @@ let kill_dummy_args ids r t =
 	let a = List.map (killrec n) a in
 	let a = List.map (ast_lift k) a in
 	let a = select_via_bl bl (a @ (eta_args k)) in
-	named_lams (list_firstn k ids) (MLapp (ast_lift k e, a))
+	named_lams (List.firstn k ids) (MLapp (ast_lift k e, a))
     | e when found n e ->
 	let a = select_via_bl bl (eta_args m) in
 	named_lams ids (MLapp (ast_lift m e, a))
@@ -1153,7 +1212,7 @@ let normalize a =
   let o = optims () in
   let rec norm a =
     let a' = if o.opt_kill_dum then kill_dummy (simpl o a) else simpl o a in
-    if a = a' then a else norm a'
+    if eq_ml_ast a a' then a else norm a'
   in norm a
 
 (*S Special treatment of fixpoint for pretty-printing purpose. *)
@@ -1165,7 +1224,7 @@ let general_optimize_fix f ids n args m c =
     | MLrel j when v.(j-1)>=0 ->
 	if ast_occurs (j+1) c then raise Impossible else v.(j-1)<-(-i-1)
     | _ -> raise Impossible
-  in list_iter_i aux args;
+  in List.iteri aux args;
   let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in
   let new_f = anonym_tmp_lams (MLapp (MLrel (n+m+1),args_f)) m in
   let new_c = named_lams ids (normalize (MLapp ((ast_subst new_f c),args))) in
@@ -1176,7 +1235,7 @@ let optimize_fix a =
   else
     let ids,a' = collect_lams a in
     let n = List.length ids in
-    if n = 0 then a
+    if Int.equal n 0 then a
     else match a' with
       | MLfix(_,[|f|],[|c|]) ->
 	  let new_f = MLapp (MLrel (n+1),eta_args n) in
@@ -1244,7 +1303,7 @@ let rec non_stricts add cand = function
       let cand = if add then 1::cand else cand in
       pop 1 (non_stricts add cand t)
   | MLrel n ->
-      List.filter ((<>) n) cand
+      List.filter (fun m -> not (Int.equal m n)) cand
   | MLapp (t,l)->
       let cand = non_stricts false cand t in
       List.fold_left (non_stricts false) cand l
@@ -1268,7 +1327,7 @@ let rec non_stricts add cand = function
 	   let n = List.length i in
 	   let cand = lift n cand in
 	   let cand = pop n (non_stricts add cand t) in
-	   Sort.merge (<=) cand c) [] v
+	   List.merge Int.compare cand c) [] v
 	(* [merge] may duplicates some indices, but I don't mind. *)
   | MLmagic t ->
       non_stricts add cand t
@@ -1304,7 +1363,7 @@ let is_not_strict t =
    restriction for the moment.
 *)
 
-open Declarations
+open Declareops
 
 let inline_test r t =
   if not (auto_inline ()) then false
@@ -1312,7 +1371,7 @@ let inline_test r t =
     let c = match r with ConstRef c -> c | _ -> assert false in
     let has_body =
       try constant_has_body (Global.lookup_constant c)
-      with e when Errors.noncritical e -> false
+      with Not_found -> false
     in
     has_body &&
       (let t1 = eta_red t in
@@ -1320,10 +1379,8 @@ let inline_test r t =
        not (is_fix t2) && ml_size t < 12 && is_not_strict t)
 
 let con_of_string s =
-  let null = empty_dirpath in
-  match repr_dirpath (dirpath_of_string s) with
-    | id :: d -> make_con (MPfile (make_dirpath d)) null (label_of_id id)
-    | [] -> assert false
+  let d, id = Libnames.split_dirpath (dirpath_of_string s) in
+  Constant.make2 (MPfile d) (Label.of_id id)
 
 let manual_inline_set =
   List.fold_right (fun x -> Cset_env.add (con_of_string x))
@@ -1355,6 +1412,6 @@ let inline r t =
   not (to_keep r) (* The user DOES want to keep it *)
   && not (is_inline_custom r)
   && (to_inline r (* The user DOES want to inline it *)
-     || (lang () <> Haskell && not (is_projection r) &&
+     || (lang () != Haskell && not (is_projection r) &&
          (is_recursor r || manual_inline r || inline_test r t)))
 
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 94e6ae69..0a71d2c8 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -1,15 +1,13 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Util
 open Names
-open Term
-open Libnames
+open Globnames
 open Miniml
 open Table
 
@@ -68,6 +66,7 @@ val type_to_signature : abbrev_map -> ml_type -> signature
 val type_expunge : abbrev_map -> ml_type -> ml_type
 val type_expunge_from_sign : abbrev_map -> signature -> ml_type -> ml_type
 
+val eq_ml_type : ml_type -> ml_type -> bool
 val isDummy : ml_type -> bool
 val isKill : sign -> bool
 
@@ -78,10 +77,10 @@ val term_expunge : signature -> ml_ident list * ml_ast -> ml_ast
 (*s Special identifiers. [dummy_name] is to be used for dead code
     and will be printed as [_] in concrete (Caml) code. *)
 
-val anonymous_name : identifier
-val dummy_name : identifier
-val id_of_name : name -> identifier
-val id_of_mlid : ml_ident -> identifier
+val anonymous_name : Id.t
+val dummy_name : Id.t
+val id_of_name : Name.t -> Id.t
+val id_of_mlid : ml_ident -> Id.t
 val tmp_id : ml_ident -> ml_ident
 
 (*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 2c923241..8158ac64 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -1,27 +1,25 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 open Names
-open Declarations
-open Environ
-open Libnames
+open Globnames
+open Errors
 open Util
 open Miniml
 open Table
 open Mlutil
-open Mod_subst
 
 (*S Functions upon ML modules. *)
 
 let rec msid_of_mt = function
   | MTident mp -> mp
   | MTwith(mt,_)-> msid_of_mt mt
-  | _ -> anomaly "Extraction:the With operator isn't applied to a name"
+  | _ -> anomaly ~label:"extraction" (Pp.str "the With operator isn't applied to a name")
 
 (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a
    [ml_structure]. *)
@@ -32,16 +30,16 @@ let se_iter do_decl do_spec do_mp =
     | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt'
     | MTwith (mt,ML_With_type(idl,l,t))->
 	let mp_mt = msid_of_mt mt in
-	let l',idl' = list_sep_last idl in
+	let l',idl' = List.sep_last idl in
 	let mp_w =
-	  List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
+	  List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl'
 	in
-	let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l')) in
+	let r = ConstRef (Constant.make2 mp_w (Label.of_id l')) in
 	mt_iter mt; do_decl (Dtype(r,l,t))
     | MTwith (mt,ML_With_module(idl,mp))->
         let mp_mt = msid_of_mt mt in
         let mp_w =
-	  List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl
+	  List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl
 	in
 	mt_iter mt; do_mp mp_w; do_mp mp
     | MTsig (_, sign) -> List.iter spec_iter sign
@@ -110,13 +108,13 @@ let ind_iter_references do_term do_cons do_type kn ind =
   let cons_iter cp l = do_cons (ConstructRef cp); List.iter type_iter l in
   let packet_iter ip p =
     do_type (IndRef ip);
-    if lang () = Ocaml then
+    if lang () == Ocaml then
       (match ind.ind_equiv with
 	 | Miniml.Equiv kne -> do_type (IndRef (mind_of_kn kne, snd ip));
 	 | _ -> ());
     Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types
   in
-  if lang () = Ocaml then record_iter_references do_term ind.ind_kind;
+  if lang () == Ocaml then record_iter_references do_term ind.ind_kind;
     Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets
 
 let decl_iter_references do_term do_cons do_type =
@@ -199,6 +197,11 @@ let rec msig_of_ms = function
 let signature_of_structure s =
   List.map (fun (mp,ms) -> mp,msig_of_ms ms) s
 
+let rec mtyp_of_mexpr = function
+  | MEfunctor (id,ty,e) -> MTfunsig (id,ty, mtyp_of_mexpr e)
+  | MEstruct (mp,str) -> MTsig (mp, msig_of_ms str)
+  | _ -> assert false
+
 
 (*s Searching one [ml_decl] in a [ml_structure] by its [global_reference] *)
 
@@ -208,18 +211,18 @@ let is_modular = function
 
 let rec search_structure l m = function
   | [] -> raise Not_found
-  | (lab,d)::_ when lab=l && is_modular d = m -> d
+  | (lab,d)::_ when Label.equal lab l && (is_modular d : bool) == m -> d
   | _::fields -> search_structure l m fields
 
 let get_decl_in_structure r struc =
   try
     let base_mp,ll = labels_of_ref r in
     if not (at_toplevel base_mp) then error_not_visible r;
-    let sel = List.assoc base_mp struc in
+    let sel = List.assoc_f ModPath.equal base_mp struc in
     let rec go ll sel = match ll with
       | [] -> assert false
       | l :: ll ->
-	  match search_structure l (ll<>[]) sel with
+	  match search_structure l (not (List.is_empty ll)) sel with
 	    | SEdecl d -> d
 	    | SEmodtype m -> assert false
 	    | SEmodule m ->
@@ -228,7 +231,7 @@ let get_decl_in_structure r struc =
 		  | _ -> error_not_visible r
     in go ll sel
   with Not_found ->
-    anomaly "reference not found in extracted structure"
+    anomaly (Pp.str "reference not found in extracted structure")
 
 
 (*s Optimization of a [ml_structure]. *)
@@ -251,7 +254,7 @@ let dfix_to_mlfix rv av i =
 	(try MLrel (n + (Refmap'.find refe s)) with Not_found -> t)
     | _ -> ast_map_lift subst n t
   in
-  let ids = Array.map (fun r -> id_of_label (label_of_r r)) rv in
+  let ids = Array.map (fun r -> Label.to_id (label_of_r r)) rv in
   let c = Array.map (subst 0) av
   in MLfix(i, ids, c)
 
@@ -297,8 +300,6 @@ and optim_me to_appear s = function
    For non-library extraction, we recompute a minimal set of dependencies
    for first-level definitions (no module pruning yet). *)
 
-exception NoDepCheck
-
 let base_r = function
   | ConstRef c as r -> r
   | IndRef (kn,_) -> IndRef (kn,0)
@@ -353,7 +354,7 @@ let rec depcheck_se = function
     let se' = depcheck_se se in
     let refs = declared_refs d in
     let refs' = List.filter is_needed refs in
-    if refs' = [] then
+    if List.is_empty refs' then
       (List.iter remove_info_axiom refs;
        List.iter remove_opaque refs;
        se')
@@ -362,7 +363,7 @@ let rec depcheck_se = function
       (* Hack to avoid extracting unused part of a Dfix *)
       match d with
 	| Dfix (rv,trms,tys) when (List.for_all is_custom refs') ->
-	  let trms' =  Array.create (Array.length rv) (MLexn "UNUSED") in
+	  let trms' =  Array.make (Array.length rv) (MLexn "UNUSED") in
 	  ((l,SEdecl (Dfix (rv,trms',tys))) :: se')
 	| _ -> (compute_deps_decl d; t::se')
     end
@@ -376,14 +377,22 @@ let rec depcheck_struct = function
   | (mp,lse)::struc ->
       let struc' = depcheck_struct struc in
       let lse' = depcheck_se lse in
-      if lse' = [] then struc' else (mp,lse')::struc'
+      if List.is_empty lse' then struc' else (mp,lse')::struc'
+
+let is_prefix pre s =
+  let len = String.length pre in
+  let rec is_prefix_aux i =
+    if Int.equal i len then true
+    else pre.[i] == s.[i] && is_prefix_aux (succ i)
+  in
+  is_prefix_aux 0
 
 let check_implicits = function
   | MLexn s ->
-      if String.length s > 8 && (s.[0] = 'U' || s.[0] = 'I') then
+      if String.length s > 8 && (s.[0] == 'U' || s.[0] == 'I') then
 	begin
-	  if String.sub s 0 7 = "UNBOUND" then assert false;
-	  if String.sub s 0 8 = "IMPLICIT" then
+	  if is_prefix "UNBOUND" s then assert false;
+	  if is_prefix "IMPLICIT" s then
 	    error_non_implicit (String.sub s 9 (String.length s - 9));
 	end;
       false
@@ -397,7 +406,7 @@ let optimize_struct to_appear struc =
   in
   ignore (struct_ast_search check_implicits opt_struc);
   if library () then
-    List.filter (fun (_,lse) -> lse<>[]) opt_struc
+    List.filter (fun (_,lse) -> not (List.is_empty lse)) opt_struc
   else begin
     reset_needed ();
     List.iter add_needed (fst to_appear);
diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli
index 58d8167d..ca32f029 100644
--- a/plugins/extraction/modutil.mli
+++ b/plugins/extraction/modutil.mli
@@ -1,17 +1,14 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
 open Names
-open Declarations
-open Environ
-open Libnames
+open Globnames
 open Miniml
-open Mod_subst
 
 (*s Functions upon ML modules. *)
 
@@ -20,11 +17,14 @@ val struct_type_search : (ml_type -> bool) -> ml_structure -> bool
 
 type do_ref = global_reference -> unit
 
+val ast_iter_references : do_ref -> do_ref -> do_ref -> ml_ast -> unit
 val decl_iter_references : do_ref -> do_ref -> do_ref -> ml_decl -> unit
 val spec_iter_references : do_ref -> do_ref -> do_ref -> ml_spec -> unit
 
 val signature_of_structure : ml_structure -> ml_signature
 
+val mtyp_of_mexpr : ml_module_expr -> ml_module_type
+
 val msid_of_mt : ml_module_type -> module_path
 
 val get_decl_in_structure : global_reference -> ml_structure -> ml_decl
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 70e71eeb..30ac3d3f 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,25 +9,21 @@
 (*s Production of Ocaml syntax. *)
 
 open Pp
+open Errors
 open Util
 open Names
 open Nameops
-open Libnames
+open Globnames
 open Table
 open Miniml
 open Mlutil
 open Modutil
 open Common
-open Declarations
 
 
 (*s Some utility functions. *)
 
-let pp_tvar id =
-  let s = string_of_id id in
-  if String.length s < 2 || s.[1]<>'\''
-  then str ("'"^s)
-  else str ("' "^s)
+let pp_tvar id = str ("'" ^ Id.to_string id)
 
 let pp_abst = function
   | [] -> mt ()
@@ -36,10 +32,10 @@ let pp_abst = function
       str " ->" ++ spc ()
 
 let pp_parameters l =
-  (pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))
+  (pp_boxed_tuple pp_tvar l ++ space_if (not (List.is_empty l)))
 
 let pp_string_parameters l =
-  (pp_boxed_tuple str l ++ space_if (l<>[]))
+  (pp_boxed_tuple str l ++ space_if (not (List.is_empty l)))
 
 let pp_letin pat def body =
   let fstline = str "let " ++ pat ++ str " =" ++ spc () ++ def in
@@ -48,7 +44,7 @@ let pp_letin pat def body =
 (*s Ocaml renaming issues. *)
 
 let keywords =
-  List.fold_right (fun s -> Idset.add (id_of_string s))
+  List.fold_right (fun s -> Id.Set.add (Id.of_string s))
   [ "and"; "as"; "assert"; "begin"; "class"; "constraint"; "do";
     "done"; "downto"; "else"; "end"; "exception"; "external"; "false";
     "for"; "fun"; "function"; "functor"; "if"; "in"; "include";
@@ -57,22 +53,30 @@ let keywords =
     "parser"; "private"; "rec"; "sig"; "struct"; "then"; "to"; "true";
     "try"; "type"; "val"; "virtual"; "when"; "while"; "with"; "mod";
     "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ]
-  Idset.empty
+  Id.Set.empty
 
 let pp_open mp = str ("open "^ string_of_modfile mp ^"\n")
 
-let preamble _ used_modules usf =
+let pp_comment s = str "(* " ++ hov 0 s ++ str " *)"
+
+let pp_header_comment = function
+  | None -> mt ()
+  | Some com -> pp_comment com ++ fnl () ++ fnl ()
+
+let preamble _ comment used_modules usf =
+  pp_header_comment comment ++
   prlist pp_open used_modules ++
-  (if used_modules = [] then mt () else fnl ()) ++
+  (if List.is_empty used_modules then mt () else fnl ()) ++
   (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n" else mt()) ++
   (if usf.mldummy then
      str "let __ = let rec f _ = Obj.repr f in Obj.repr f\n"
    else mt ()) ++
   (if usf.tdummy || usf.tunknown || usf.mldummy then fnl () else mt ())
 
-let sig_preamble _ used_modules usf =
+let sig_preamble _ comment used_modules usf =
+  pp_header_comment comment ++ fnl () ++ fnl () ++
   prlist pp_open used_modules ++
-  (if used_modules = [] then mt () else fnl ()) ++
+  (if List.is_empty used_modules then mt () else fnl ()) ++
   (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n\n" else mt())
 
 (*s The pretty-printer for Ocaml syntax*)
@@ -93,7 +97,7 @@ let is_infix r =
   is_inline_custom r &&
   (let s = find_custom r in
    let l = String.length s in
-   l >= 2 && s.[0] = '(' && s.[l-1] = ')')
+   l >= 2 && s.[0] == '(' && s.[l-1] == ')')
 
 let get_infix r =
   let s = find_custom r in
@@ -110,22 +114,21 @@ let pp_one_field r i = function
 
 let pp_field r fields i = pp_one_field r i (List.nth fields i)
 
-let pp_fields r fields = list_map_i (pp_one_field r) 0 fields
+let pp_fields r fields = List.map_i (pp_one_field r) 0 fields
 
 (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
     are needed or not. *)
 
-let rec pp_type par vl t =
+let pp_type par vl t =
   let rec pp_rec par = function
     | Tmeta _ | Tvar' _ | Taxiom -> assert false
     | Tvar i -> (try pp_tvar (List.nth vl (pred i))
-		 with e when Errors.noncritical e ->
-                   (str "'a" ++ int i))
+                 with Failure _ -> (str "'a" ++ int i))
     | 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 not (keep_singleton ()) && kn = mk_ind "Coq.Init.Specif" "sig" ->
+	when not (keep_singleton ()) && MutInd.equal 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
@@ -149,7 +152,7 @@ let is_bool_patt p s =
       | Pcons (r,[]) -> r
       | _ -> raise Not_found
     in
-    find_custom r = s
+    String.equal (find_custom r) s
   with Not_found -> false
 
 
@@ -186,7 +189,7 @@ let rec pp_expr par env args =
 	hv 0 (apply2 (pp_letin pp_id pp_a1 pp_a2))
     | MLglob r ->
 	(try
-	   let args = list_skipn (projection_arity r) args in
+	   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 e when Errors.noncritical e -> apply (pp_global Term r))
@@ -203,35 +206,35 @@ let rec pp_expr par env args =
     | MLaxiom ->
 	pp_par par (str "failwith \"AXIOM TO BE REALIZED\"")
     | MLcons (_,r,a) as c ->
-        assert (args=[]);
+        assert (List.is_empty 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 ne = not (List.is_empty 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
+	    if not (List.is_empty 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 *)
+	      if String.is_empty (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 = []);
+        assert (List.is_empty 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
+	  if not (List.is_empty 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
@@ -250,7 +253,7 @@ let rec pp_expr par env args =
         (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
+	   if Int.equal (Array.length pv) 1 then
 	     let s1,s2 = pp_one_pat env pv.(0) in
 	     hv 0 (apply2 (pp_letin s1 head s2))
 	   else
@@ -265,8 +268,8 @@ let rec pp_expr par env args =
 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 List.is_empty fields then raise Impossible;
+  if not (Int.equal (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
@@ -277,7 +280,7 @@ and pp_record_proj par env typ t pv args =
     | _ -> 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
+    | Prel j :: l -> if Int.equal i j then idx else lookup_rel i (idx+1) l
     | Pwild :: l -> lookup_rel i (idx+1) l
     | _ -> raise Impossible
   in
@@ -301,15 +304,15 @@ and pp_record_pat (fields, args) =
    str " }"
 
 and pp_cons_pat r ppl =
-  if is_infix r && List.length ppl = 2 then
+  if is_infix r && Int.equal (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
+    if not (List.is_empty fields) then pp_record_pat (pp_fields r fields, ppl)
+    else if String.is_empty (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
+      pp_global Cons r ++ space_if (not (List.is_empty 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)
@@ -339,7 +342,7 @@ and pp_pat env pv =
     (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 = Array.length pv - 1 then mt () else fnl ())
+       if Int.equal i (Array.length pv - 1) then mt () else fnl ())
     pv
 
 and pp_function env t =
@@ -347,7 +350,7 @@ and pp_function env t =
   let bl,env' = push_vars (List.map id_of_mlid bl) env in
   match t' with
     | MLcase(Tglob(r,_),MLrel 1,pv) when
-	not (is_coinductive r) && get_record_fields r = [] &&
+	not (is_coinductive r) && List.is_empty (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)) ++
@@ -371,7 +374,7 @@ and pp_fix par env i (ids,bl) args =
 	  prvect_with_sep
       	    (fun () -> fnl () ++ str "and ")
 	    (fun (fi,ti) -> pr_id fi ++ pp_function env ti)
-	    (array_map2 (fun id b -> (id,b)) ids bl) ++
+	    (Array.map2 (fun id b -> (id,b)) ids bl) ++
 	  fnl () ++
 	  hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))
 
@@ -390,7 +393,7 @@ let pp_Dfix (rv,c,t) =
       (if init then failwith "empty phrase" else mt ())
     else
       let void = is_inline_custom rv.(i) ||
-	(not (is_custom rv.(i)) && c.(i) = MLexn "UNUSED")
+	(not (is_custom rv.(i)) && match c.(i) with MLexn "UNUSED" -> true | _ -> false)
       in
       if void then pp init (i+1)
       else
@@ -413,20 +416,19 @@ let pp_equiv param_list name = function
   | RenEquiv ren, _  ->
       str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name
 
-let pp_comment s = str "(* " ++ s ++ str " *)"
 
 let pp_one_ind prefix ip_equiv pl name cnames ctyps =
   let pl = rename_tvars keywords pl in
   let pp_constructor i typs =
-    (if i=0 then mt () else fnl ()) ++
+    (if Int.equal i 0 then mt () else fnl ()) ++
     hov 3 (str "| " ++ cnames.(i) ++
-	   (if typs = [] then mt () else str " of ") ++
+	   (if List.is_empty typs then mt () else str " of ") ++
 	   prlist_with_sep
 	    (fun () -> spc () ++ str "* ") (pp_type true pl) typs)
   in
   pp_parameters pl ++ str prefix ++ name ++
   pp_equiv pl name ip_equiv ++ str " =" ++
-  if Array.length ctyps = 0 then str " unit (* empty inductive *)"
+  if Int.equal (Array.length ctyps) 0 then str " unit (* empty inductive *)"
   else fnl () ++ v 0 (prvecti pp_constructor ctyps)
 
 let pp_logical_ind packet =
@@ -525,7 +527,7 @@ let pp_decl = function
 	    pp_string_parameters ids, str "=" ++ spc () ++ str s
 	  with Not_found ->
 	    pp_parameters l,
-	    if t = Taxiom then str "(* AXIOM TO BE REALIZED *)"
+	    if t == Taxiom then str "(* AXIOM TO BE REALIZED *)"
 	    else str "=" ++ spc () ++ pp_type false l t
 	in
 	hov 2 (str "type " ++ ids ++ name ++ spc () ++ def)
@@ -632,7 +634,7 @@ and pp_module_type params = function
       str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
   | MTsig (mp, sign) ->
       push_visible mp params;
-      let l = map_succeed pp_specif sign in
+      let l = List.map pp_specif sign in
       pop_visible ();
       str "sig " ++ fnl () ++
       v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
@@ -640,11 +642,11 @@ and pp_module_type params = function
   | MTwith(mt,ML_With_type(idl,vl,typ)) ->
       let ids = pp_parameters (rename_tvars keywords vl) in
       let mp_mt = msid_of_mt mt in
-      let l,idl' = list_sep_last idl in
+      let l,idl' = List.sep_last idl in
       let mp_w =
-	List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl'
+	List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl'
       in
-      let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l)) in
+      let r = ConstRef (Constant.make2 mp_w (Label.of_id l)) in
       push_visible mp_mt [];
       let pp_w = str " with type " ++ ids ++ pp_global Type r in
       pop_visible();
@@ -652,7 +654,7 @@ and pp_module_type params = function
   | MTwith(mt,ML_With_module(idl,mp)) ->
       let mp_mt = msid_of_mt mt in
       let mp_w =
-	List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) mp_mt idl
+	List.fold_left (fun mp id -> MPdot(mp,Label.of_id id)) mp_mt idl
       in
       push_visible mp_mt [];
       let pp_w = str " with module " ++ pp_modname mp_w in
@@ -672,7 +674,7 @@ let rec pp_structure_elem = function
   | (l,SEmodule m) ->
       let typ =
         (* virtual printing of the type, in order to have a correct mli later*)
-	if Common.get_phase () = Pre then
+	if Common.get_phase () == Pre then
 	  str ": " ++ pp_module_type [] m.ml_mod_type
 	else mt ()
       in
@@ -705,7 +707,7 @@ and pp_module_expr params = function
       str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def
   | MEstruct (mp, sel) ->
       push_visible mp params;
-      let l = map_succeed pp_structure_elem sel in
+      let l = List.map pp_structure_elem sel in
       pop_visible ();
       str "struct " ++ fnl () ++
       v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
diff --git a/plugins/extraction/ocaml.mli b/plugins/extraction/ocaml.mli
index 36035b5a..4e796792 100644
--- a/plugins/extraction/ocaml.mli
+++ b/plugins/extraction/ocaml.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index f7fa3383..69dea25a 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -9,10 +9,9 @@
 (*s Production of Scheme syntax. *)
 
 open Pp
+open Errors
 open Util
 open Names
-open Nameops
-open Libnames
 open Miniml
 open Mlutil
 open Table
@@ -21,22 +20,29 @@ open Common
 (*s Scheme renaming issues. *)
 
 let keywords =
-  List.fold_right (fun s -> Idset.add (id_of_string s))
+  List.fold_right (fun s -> Id.Set.add (Id.of_string s))
     [ "define"; "let"; "lambda"; "lambdas"; "match";
       "apply"; "car"; "cdr";
       "error"; "delay"; "force"; "_"; "__"]
-    Idset.empty
+    Id.Set.empty
 
-let preamble _ _ usf =
+let pp_comment s = str";; "++h 0 s++fnl ()
+
+let pp_header_comment = function
+  | None -> mt ()
+  | Some com -> pp_comment com ++ fnl () ++ fnl ()
+
+let preamble _ comment _ usf =
+  pp_header_comment comment ++
   str ";; This extracted scheme code relies on some additional macros\n" ++
-  str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme\n" ++
+  str ";; available at http://www.pps.univ-paris-diderot.fr/~letouzey/scheme\n" ++
   str "(load \"macros_extr.scm\")\n\n" ++
   (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ())
 
 let pr_id id =
-  let s = string_of_id id in
+  let s = Id.to_string id in
   for i = 0 to String.length s - 1 do
-    if s.[i] = '\'' then s.[i] <- '~'
+    if s.[i] == '\'' then s.[i] <- '~'
   done;
   str s
 
@@ -86,11 +92,11 @@ let rec pp_expr env args =
     | MLglob r ->
 	apply (pp_global Term r)
     | MLcons (_,r,args') ->
-	assert (args=[]);
+	assert (List.is_empty args);
 	let st =
 	  str "`" ++
 	  paren (pp_global Cons r ++
-		 (if args' = [] then mt () else spc ()) ++
+		 (if List.is_empty args' then mt () else spc ()) ++
 		 prlist_with_sep spc (pp_cons_args env) args')
 	in
 	if is_coinductive r then paren (str "delay " ++ st) else st
@@ -99,7 +105,7 @@ let rec pp_expr env args =
 	error "Cannot handle general patterns in Scheme yet."
     | MLcase (_,t,pv) when is_custom_match pv ->
 	let mkfun (ids,_,e) =
-	  if ids <> [] then named_lams (List.rev ids) e
+	  if not (List.is_empty ids) then named_lams (List.rev ids) e
 	  else dummy_lams (ast_lift 1 e) 1
 	in
 	apply
@@ -129,7 +135,7 @@ let rec pp_expr env args =
 and pp_cons_args env = function
   | MLcons (_,r,args) when is_coinductive r ->
       paren (pp_global Cons r ++
-	     (if args = [] then mt () else spc ()) ++
+	     (if List.is_empty args then mt () else spc ()) ++
 	     prlist_with_sep spc (pp_cons_args env) args)
   | e -> str "," ++ pp_expr env [] e
 
@@ -141,7 +147,7 @@ and pp_one_pat env (ids,p,t) =
   in
   let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
   let args =
-    if ids = [] then mt ()
+    if List.is_empty ids then mt ()
     else (str " " ++ prlist_with_sep spc pr_id (List.rev ids))
   in
   (pp_global Cons r ++ args), (pp_expr env' [] t)
@@ -161,7 +167,7 @@ and pp_fix env j (ids,bl) args =
 	       (prvect_with_sep fnl
 		  (fun (fi,ti) ->
 		     paren ((pr_id fi) ++ spc () ++ (pp_expr env [] ti)))
-		  (array_map2 (fun id b -> (id,b)) ids bl)) ++
+		  (Array.map2 (fun id b -> (id,b)) ids bl)) ++
 	     fnl () ++
       	     hov 2 (pp_apply (pr_id (ids.(j))) true args))))
 
@@ -177,7 +183,7 @@ let pp_decl = function
       prvecti
 	(fun i r ->
 	  let void = is_inline_custom r ||
-	    (not (is_custom r) && defs.(i) = MLexn "UNUSED")
+	    (not (is_custom r) && match defs.(i) with MLexn "UNUSED" -> true | _ -> false)
 	  in
 	  if void then mt ()
 	  else
@@ -222,7 +228,7 @@ let scheme_descr = {
   preamble = preamble;
   pp_struct = pp_struct;
   sig_suffix = None;
-  sig_preamble = (fun _ _ _ -> mt ());
+  sig_preamble = (fun _ _ _ _ -> mt ());
   pp_sig = (fun _ -> mt ());
   pp_decl = pp_decl;
 }
diff --git a/plugins/extraction/scheme.mli b/plugins/extraction/scheme.mli
index 2a2bf48e..f0e36e09 100644
--- a/plugins/extraction/scheme.mli
+++ b/plugins/extraction/scheme.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index eaa64fef..44d760cc 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -11,10 +11,11 @@ open Term
 open Declarations
 open Nameops
 open Namegen
-open Summary
 open Libobject
 open Goptions
 open Libnames
+open Globnames
+open Errors
 open Util
 open Pp
 open Miniml
@@ -22,14 +23,14 @@ open Miniml
 (** Sets and maps for [global_reference] that use the "user" [kernel_name]
     instead of the canonical one *)
 
-module Refmap' = Map.Make(RefOrdered_env)
-module Refset' = Set.Make(RefOrdered_env)
+module Refmap' = Refmap_env
+module Refset' = Refset_env
 
 (*S Utilities about [module_path] and [kernel_names] and [global_reference] *)
 
 let occur_kn_in_ref kn = function
   | IndRef (kn',_)
-  | ConstructRef ((kn',_),_) -> kn = kn'
+  | ConstructRef ((kn',_),_) -> Names.eq_mind kn kn'
   | ConstRef _ -> false
   | VarRef _ -> assert false
 
@@ -54,21 +55,19 @@ let is_modfile = function
   | _ -> false
 
 let raw_string_of_modfile = function
-  | MPfile f -> String.capitalize (string_of_id (List.hd (repr_dirpath f)))
+  | MPfile f -> String.capitalize (Id.to_string (List.hd (DirPath.repr f)))
   | _ -> assert false
 
-let current_toplevel () = fst (Lib.current_prefix ())
-
 let is_toplevel mp =
-  mp = initial_path || mp = current_toplevel ()
+  ModPath.equal mp initial_path || ModPath.equal mp (Lib.current_mp ())
 
 let at_toplevel mp =
   is_modfile mp || is_toplevel mp
 
-let rec mp_length mp =
-  let mp0 = current_toplevel () in
+let mp_length mp =
+  let mp0 = Lib.current_mp () in
   let rec len = function
-    | mp when mp = mp0 -> 1
+    | mp when ModPath.equal mp mp0 -> 1
     | MPdot (mp,_) -> 1 + len mp
     | _ -> 1
   in len mp
@@ -80,7 +79,7 @@ let rec prefixes_mp mp = match mp with
   | _ -> MPset.singleton mp
 
 let rec get_nth_label_mp n = function
-  | MPdot (mp,l) -> if n=1 then l else get_nth_label_mp (n-1) mp
+  | MPdot (mp,l) -> if Int.equal n 1 then l else get_nth_label_mp (n-1) mp
   | _ -> failwith "get_nth_label: not enough MPdot"
 
 let common_prefix_from_list mp0 mpl =
@@ -91,12 +90,12 @@ let common_prefix_from_list mp0 mpl =
   in f mpl
 
 let rec parse_labels2 ll mp1 = function
-  | mp when mp1=mp -> mp,ll
+  | mp when ModPath.equal mp1 mp -> mp,ll
   | MPdot (mp,l) -> parse_labels2 (l::ll) mp1 mp
   | mp -> mp,ll
 
 let labels_of_ref r =
-  let mp_top = current_toplevel () in
+  let mp_top = Lib.current_mp () in
   let mp,_,l = repr_of_r r in
   parse_labels2 [l] mp_top mp
 
@@ -138,7 +137,7 @@ let is_coinductive r =
     | IndRef (kn,_) -> kn
     | _ -> assert false
   in
-  try Mindmap_env.find kn !inductive_kinds = Coinductive
+  try Mindmap_env.find kn !inductive_kinds == Coinductive
   with Not_found -> false
 
 let is_coinductive_type = function
@@ -163,40 +162,39 @@ let record_fields_of_type = function
 (*s Recursors table. *)
 
 (* NB: here we can use the equivalence between canonical
-   and user constant names : Cset is fine, no need for [Cset_env] *)
+   and user constant names. *)
 
-let recursors = ref Cset.empty
-let init_recursors () = recursors := Cset.empty
+let recursors = ref KNset.empty
+let init_recursors () = recursors := KNset.empty
 
-let add_recursors env kn =
-  let mk_con id =
-    make_con_equiv
-      (modpath (user_mind kn))
-      (modpath (canonical_mind kn))
-      empty_dirpath (label_of_id id)
+let add_recursors env ind =
+  let kn = MutInd.canonical ind in
+  let mk_kn id =
+    KerName.make (KerName.modpath kn) DirPath.empty (Label.of_id id)
   in
-  let mib = Environ.lookup_mind kn env in
+  let mib = Environ.lookup_mind ind env in
   Array.iter
     (fun mip ->
        let id = mip.mind_typename in
-       let c_rec = mk_con (Nameops.add_suffix id "_rec")
-       and c_rect = mk_con (Nameops.add_suffix id "_rect") in
-       recursors := Cset.add c_rec (Cset.add c_rect !recursors))
+       let kn_rec = mk_kn (Nameops.add_suffix id "_rec")
+       and kn_rect = mk_kn (Nameops.add_suffix id "_rect") in
+       recursors := KNset.add kn_rec (KNset.add kn_rect !recursors))
     mib.mind_packets
 
 let is_recursor = function
-  | ConstRef kn -> Cset.mem kn !recursors
+  | ConstRef c -> KNset.mem (Constant.canonical c) !recursors
   | _ -> false
 
 (*s Record tables. *)
 
 (* NB: here, working modulo name equivalence is ok *)
 
-let projs = ref (Refmap.empty : int Refmap.t)
+let projs = ref (Refmap.empty : (inductive*int) Refmap.t)
 let init_projs () = projs := Refmap.empty
-let add_projection n kn = projs := Refmap.add (ConstRef kn) n !projs
+let add_projection n kn ip = projs := Refmap.add (ConstRef kn) (ip,n) !projs
 let is_projection r = Refmap.mem r !projs
-let projection_arity r = Refmap.find r !projs
+let projection_arity r = snd (Refmap.find r !projs)
+let projection_info r = Refmap.find r !projs
 
 (*s Table of used axioms *)
 
@@ -240,11 +238,11 @@ 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"
+      anomaly (Pp.str "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)
+    | ConstRef kn -> Label.to_id (con_label kn)
+    | IndRef (kn,0) -> Label.to_id (mind_label kn)
     | IndRef (kn,i) ->
       (try (snd (lookup_ind kn)).ind_packets.(i).ip_typename
        with Not_found -> last_chance r)
@@ -254,8 +252,8 @@ let safe_basename_of_global r =
     | VarRef _ -> assert false
 
 let string_of_global r =
- try string_of_qualid (Nametab.shortest_qualid_of_global Idset.empty r)
- with e when Errors.noncritical e -> string_of_id (safe_basename_of_global r)
+ try string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty r)
+ with Not_found -> Id.to_string (safe_basename_of_global r)
 
 let safe_pr_global r = str (string_of_global r)
 
@@ -263,15 +261,15 @@ let safe_pr_global r = str (string_of_global r)
 
 let safe_pr_long_global r =
   try Printer.pr_global r
-  with e when Errors.noncritical e -> match r with
+  with Not_found -> match r with
     | ConstRef kn ->
 	let mp,_,l = repr_con kn in
-	str ((string_of_mp mp)^"."^(string_of_label l))
+	str ((string_of_mp mp)^"."^(Label.to_string l))
     | _ -> assert false
 
 let pr_long_mp mp =
-  let lid = repr_dirpath (Nametab.dirpath_of_module mp) in
-  str (String.concat "." (List.map string_of_id (List.rev lid)))
+  let lid = DirPath.repr (Nametab.dirpath_of_module mp) in
+  str (String.concat "." (List.rev_map Id.to_string lid))
 
 let pr_long_global ref = pr_path (Nametab.path_of_global ref)
 
@@ -281,18 +279,18 @@ let err s = errorlabstrm "Extraction" s
 
 let warning_axioms () =
   let info_axioms = Refset'.elements !info_axioms in
-  if info_axioms = [] then ()
+  if List.is_empty info_axioms then ()
   else begin
-    let s = if List.length info_axioms = 1 then "axiom" else "axioms" in
+    let s = if Int.equal (List.length info_axioms) 1 then "axiom" else "axioms" in
     msg_warning
       (str ("The following "^s^" must be realized in the extracted code:")
        ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global info_axioms)
        ++ str "." ++ fnl ())
   end;
   let log_axioms = Refset'.elements !log_axioms in
-  if log_axioms = [] then ()
+  if List.is_empty log_axioms then ()
   else begin
-    let s = if List.length log_axioms = 1 then "axiom was" else "axioms were"
+    let s = if Int.equal (List.length log_axioms) 1 then "axiom was" else "axioms were"
     in
     msg_warning
       (str ("The following logical "^s^" encountered:") ++
@@ -302,14 +300,11 @@ 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;
-  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.")
+  end
 
 let warning_opaques accessed =
   let opaques = Refset'.elements !opaques in
-  if opaques = [] then ()
+  if List.is_empty opaques then ()
   else
     let lst = hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques) in
     if accessed then
@@ -337,7 +332,7 @@ let warning_both_mod_and_cst q mp r =
 
 let error_axiom_scheme r i =
   err (str "The type scheme axiom " ++ spc () ++
-       safe_pr_global r ++ spc () ++ str "needs " ++ pr_int i ++
+       safe_pr_global r ++ spc () ++ str "needs " ++ int i ++
        str " type variable(s).")
 
 let check_inside_module () =
@@ -409,9 +404,9 @@ let error_MPfile_as_mod mp b =
 let msg_non_implicit r n id =
   let name = match id with
     | Anonymous -> ""
-    | Name id -> "(" ^ string_of_id id ^ ") "
+    | Name id -> "(" ^ Id.to_string id ^ ") "
   in
-  "The " ^ (ordinal n) ^ " argument " ^ name ^ "of " ^ (string_of_global r)
+  "The " ^ (String.ordinal n) ^ " argument " ^ name ^ "of " ^ (string_of_global r)
 
 let error_non_implicit msg =
   err (str (msg ^ " still occurs after extraction.") ++
@@ -420,16 +415,16 @@ let error_non_implicit msg =
 let check_loaded_modfile mp = match base_mp mp with
   | MPfile dp ->
       if not (Library.library_is_loaded dp) then begin
-	match base_mp (current_toplevel ()) with
-	  | MPfile dp' when dp<>dp' ->
-	      err (str ("Please load library "^(string_of_dirpath dp^" first.")))
+	match base_mp (Lib.current_mp ()) with
+	  | MPfile dp' when not (DirPath.equal dp dp') ->
+	      err (str ("Please load library "^(DirPath.to_string dp^" first.")))
 	  | _ -> ()
       end
   | _ -> ()
 
 let info_file f =
-  Flags.if_verbose message
-    ("The file "^f^" has been created by extraction.")
+  Flags.if_verbose msg_info
+    (str ("The file "^f^" has been created by extraction."))
 
 
 (*S The Extraction auxiliary commands *)
@@ -481,7 +476,7 @@ type opt_flag =
       opt_lin_let : bool;   (* 512 *)
       opt_lin_beta : bool } (* 1024 *)
 
-let kth_digit n k = (n land (1 lsl k) <> 0)
+let kth_digit n k = not (Int.equal (n land (1 lsl k)) 0)
 
 let flag_of_int n =
     { opt_kill_dum = kth_digit n 0;
@@ -518,7 +513,7 @@ let _ = declare_bool_option
            optdepr = false;
 	   optname = "Extraction Optimize";
 	   optkey = ["Extraction"; "Optimize"];
-	   optread = (fun () -> !int_flag_ref <> 0);
+	   optread = (fun () -> not (Int.equal !int_flag_ref 0));
 	   optwrite = (fun b -> chg_flag (if b then int_flag_init else 0))}
 
 let _ = declare_int_option
@@ -531,12 +526,37 @@ let _ = declare_int_option
                           | None -> chg_flag 0
                           | Some i -> chg_flag (max i 0))}
 
+(* This option controls whether "dummy lambda" are removed when a
+   toplevel constant is defined. *)
+let conservative_types_ref = ref false
+let conservative_types () = !conservative_types_ref
+
+let _ = declare_bool_option
+  {optsync = true;
+   optdepr = false;
+   optname = "Extraction Conservative Types";
+   optkey = ["Extraction"; "Conservative"; "Types"];
+   optread = (fun () -> !conservative_types_ref);
+   optwrite = (fun b -> conservative_types_ref := b) }
+
+
+(* Allows to print a comment at the beginning of the output files *)
+let file_comment_ref = ref ""
+let file_comment () = !file_comment_ref
+
+let _ = declare_string_option
+  {optsync = true;
+   optdepr = false;
+   optname = "Extraction File Comment";
+   optkey = ["Extraction"; "File"; "Comment"];
+   optread = (fun () -> !file_comment_ref);
+   optwrite = (fun s -> file_comment_ref := s) }
 
 (*s Extraction Lang *)
 
 type lang = Ocaml | Haskell | Scheme
 
-let lang_ref = ref Ocaml
+let lang_ref = Summary.ref Ocaml ~name:"ExtrLang"
 
 let lang () = !lang_ref
 
@@ -546,18 +566,13 @@ let extr_lang : lang -> obj =
        cache_function = (fun (_,l) -> lang_ref := l);
        load_function = (fun _ (_,l) -> lang_ref := l)}
 
-let _ = declare_summary "Extraction Lang"
-	  { freeze_function = (fun () -> !lang_ref);
-	    unfreeze_function = ((:=) lang_ref);
-	    init_function = (fun () -> lang_ref := Ocaml) }
-
 let extraction_language x = Lib.add_anonymous_leaf (extr_lang x)
 
 (*s Extraction Inline/NoInline *)
 
 let empty_inline_table = (Refset'.empty,Refset'.empty)
 
-let inline_table = ref empty_inline_table
+let inline_table = Summary.ref empty_inline_table ~name:"ExtrInline"
 
 let to_inline r = Refset'.mem r (fst !inline_table)
 
@@ -584,11 +599,6 @@ let inline_extraction : bool * global_reference list -> obj =
         (fun (s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))
     }
 
-let _ = declare_summary "Extraction Inline"
-	  { freeze_function = (fun () -> !inline_table);
-	    unfreeze_function = ((:=) inline_table);
-	    init_function = (fun () -> inline_table := empty_inline_table) }
-
 (* Grammar entries. *)
 
 let extraction_inline b l =
@@ -604,7 +614,6 @@ let extraction_inline b l =
 let print_extraction_inline () =
   let (i,n)= !inline_table in
   let i'= Refset'.filter (function ConstRef _ -> true | _ -> false) i in
-  msg
     (str "Extraction Inline:" ++ fnl () ++
      Refset'.fold
        (fun r p ->
@@ -626,15 +635,15 @@ let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ())
 
 (*s Extraction Implicit *)
 
-type int_or_id = ArgInt of int | ArgId of identifier
+type int_or_id = ArgInt of int | ArgId of Id.t
 
-let implicits_table = ref Refmap'.empty
+let implicits_table = Summary.ref Refmap'.empty ~name:"ExtrImplicit"
 
 let implicits_of_global r =
  try Refmap'.find r !implicits_table with Not_found -> []
 
 let add_implicits r l =
-  let typ = Global.type_of_global r in
+  let typ = Global.type_of_global_unsafe r in
   let rels,_ =
     decompose_prod (Reduction.whd_betadeltaiota (Global.env ()) typ) in
   let names = List.rev_map fst rels in
@@ -645,7 +654,7 @@ let add_implicits r l =
 	else err (int i ++ str " is not a valid argument number for " ++
 		  safe_pr_global r)
     | ArgId id ->
-	(try list_index (Name id) names
+	(try List.index Name.equal (Name id) names
 	 with Not_found ->
 	   err (str "No argument " ++ pr_id id ++ str " for " ++
 		safe_pr_global r))
@@ -664,11 +673,6 @@ let implicit_extraction : global_reference * int_or_id list -> obj =
        subst_function = (fun (s,(r,l)) -> (fst (subst_global s r), l))
     }
 
-let _ = declare_summary "Extraction Implicit"
-	  { freeze_function = (fun () -> !implicits_table);
-	    unfreeze_function = ((:=) implicits_table);
-	    init_function = (fun () -> implicits_table := Refmap'.empty) }
-
 (* Grammar entries. *)
 
 let extraction_implicit r l =
@@ -678,21 +682,21 @@ let extraction_implicit r l =
 
 (*s Extraction Blacklist of filenames not to use while extracting *)
 
-let blacklist_table = ref Idset.empty
+let blacklist_table = Summary.ref Id.Set.empty ~name:"ExtrBlacklist"
 
 let modfile_ids = ref []
 let modfile_mps = ref MPmap.empty
 
 let reset_modfile () =
-  modfile_ids := Idset.elements !blacklist_table;
+  modfile_ids := Id.Set.elements !blacklist_table;
   modfile_mps := MPmap.empty
 
 let string_of_modfile mp =
   try MPmap.find mp !modfile_mps
   with Not_found ->
-    let id = id_of_string (raw_string_of_modfile mp) in
+    let id = Id.of_string (raw_string_of_modfile mp) in
     let id' = next_ident_away id !modfile_ids in
-    let s' = string_of_id id' in
+    let s' = Id.to_string id' in
     modfile_ids := id' :: !modfile_ids;
     modfile_mps := MPmap.add mp s' !modfile_mps;
     s'
@@ -701,16 +705,16 @@ let string_of_modfile mp =
 
 let file_of_modfile mp =
   let s0 = match mp with
-    | MPfile f -> string_of_id (List.hd (repr_dirpath f))
+    | MPfile f -> Id.to_string (List.hd (DirPath.repr f))
     | _ -> assert false
   in
   let s = String.copy (string_of_modfile mp) in
-  if s.[0] <> s0.[0] then s.[0] <- s0.[0];
+  if s.[0] != s0.[0] then s.[0] <- s0.[0];
   s
 
 let add_blacklist_entries l =
   blacklist_table :=
-    List.fold_right (fun s -> Idset.add (id_of_string (String.capitalize s)))
+    List.fold_right (fun s -> Id.Set.add (Id.of_string (String.capitalize s)))
       l !blacklist_table
 
 (* Registration of operations for rollback. *)
@@ -723,40 +727,33 @@ let blacklist_extraction : string list -> obj =
        subst_function = (fun (_,x) -> x)
     }
 
-let _ = declare_summary "Extraction Blacklist"
-	  { freeze_function = (fun () -> !blacklist_table);
-	    unfreeze_function = ((:=) blacklist_table);
-	    init_function = (fun () -> blacklist_table := Idset.empty) }
-
 (* Grammar entries. *)
 
 let extraction_blacklist l =
-  let l = List.rev_map string_of_id l in
+  let l = List.rev_map Id.to_string l in
   Lib.add_anonymous_leaf (blacklist_extraction l)
 
 (* Printing part *)
 
 let print_extraction_blacklist () =
-  msgnl
-    (prlist_with_sep fnl pr_id (Idset.elements !blacklist_table))
+  prlist_with_sep fnl pr_id (Id.Set.elements !blacklist_table)
 
 (* Reset part *)
 
 let reset_blacklist : unit -> obj =
   declare_object
     {(default_object "Reset Extraction Blacklist") with
-       cache_function = (fun (_,_)-> blacklist_table := Idset.empty);
-       load_function = (fun _ (_,_)-> blacklist_table := Idset.empty)}
+       cache_function = (fun (_,_)-> blacklist_table := Id.Set.empty);
+       load_function = (fun _ (_,_)-> blacklist_table := Id.Set.empty)}
 
 let reset_extraction_blacklist () = Lib.add_anonymous_leaf (reset_blacklist ())
 
 (*s Extract Constant/Inductive. *)
 
 (* UGLY HACK: to be defined in [extraction.ml] *)
-let use_type_scheme_nb_args, register_type_scheme_nb_args =
-  let r = ref (fun _ _ -> 0) in (fun x y -> !r x y), (:=) r
+let (use_type_scheme_nb_args, type_scheme_nb_args_hook) = Hook.make ()
 
-let customs = ref Refmap'.empty
+let customs = Summary.ref Refmap'.empty ~name:"ExtrCustom"
 
 let add_custom r ids s = customs := Refmap'.add r (ids,s) !customs
 
@@ -768,13 +765,13 @@ let find_custom r = snd (Refmap'.find r !customs)
 
 let find_type_custom r = Refmap'.find r !customs
 
-let custom_matchs = ref Refmap'.empty
+let custom_matchs = Summary.ref Refmap'.empty ~name:"ExtrCustomMatchs"
 
 let add_custom_match r s =
   custom_matchs := Refmap'.add r s !custom_matchs
 
 let indref_of_match pv =
-  if Array.length pv = 0 then raise Not_found;
+  if Array.is_empty pv then raise Not_found;
   let (_,pat,_) = pv.(0) in
   match pat with
     | Pusual (ConstructRef (ip,_)) -> IndRef ip
@@ -800,11 +797,6 @@ let in_customs : global_reference * string list * string -> obj =
         (fun (s,(r,ids,str)) -> (fst (subst_global s r), ids, str))
     }
 
-let _ = declare_summary "ML extractions"
-	  { freeze_function = (fun () -> !customs);
-	    unfreeze_function = ((:=) customs);
-	    init_function = (fun () -> customs := Refmap'.empty) }
-
 let in_custom_matchs : global_reference * string -> obj =
   declare_object
     {(default_object "ML extractions custom matchs") with
@@ -814,11 +806,6 @@ let in_custom_matchs : global_reference * string -> obj =
        subst_function = (fun (subs,(r,s)) -> (fst (subst_global subs r), s))
     }
 
-let _ = declare_summary "ML extractions custom match"
-	  { freeze_function = (fun () -> !custom_matchs);
-	    unfreeze_function = ((:=) custom_matchs);
-	    init_function = (fun () -> custom_matchs := Refmap'.empty) }
-
 (* Grammar entries. *)
 
 let extract_constant_inline inline r ids s =
@@ -827,12 +814,12 @@ let extract_constant_inline inline r ids s =
   match g with
     | ConstRef kn ->
 	let env = Global.env () in
-	let typ = Typeops.type_of_constant env kn in
+	let typ = Global.type_of_global_unsafe (ConstRef kn) in
 	let typ = Reduction.whd_betadeltaiota env typ in
 	if Reduction.is_arity env typ
 	  then begin
-	    let nargs = use_type_scheme_nb_args env typ in
-	    if List.length ids <> nargs then error_axiom_scheme g nargs
+	    let nargs = Hook.get use_type_scheme_nb_args env typ in
+	    if not (Int.equal (List.length ids) nargs) then error_axiom_scheme g nargs
 	  end;
 	Lib.add_anonymous_leaf (inline_extraction (inline,[g]));
 	Lib.add_anonymous_leaf (in_customs (g,ids,s))
@@ -847,12 +834,12 @@ let extract_inductive r s l optstr =
     | IndRef ((kn,i) as ip) ->
 	let mib = Global.lookup_mind kn in
 	let n = Array.length mib.mind_packets.(i).mind_consnames in
-	if n <> List.length l then error_nb_cons ();
+	if not (Int.equal n (List.length l)) then error_nb_cons ();
 	Lib.add_anonymous_leaf (inline_extraction (true,[g]));
 	Lib.add_anonymous_leaf (in_customs (g,[],s));
 	Option.iter (fun s -> Lib.add_anonymous_leaf (in_custom_matchs (g,s)))
 	  optstr;
-	list_iter_i
+	List.iteri
 	  (fun j s ->
 	     let g = ConstructRef (ip,succ j) in
 	     Lib.add_anonymous_leaf (inline_extraction (true,[g]));
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 14792f8f..1acbe355 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,13 +8,14 @@
 
 open Names
 open Libnames
+open Globnames
 open Miniml
 open Declarations
 
-module Refset' : Set.S with type elt = global_reference
+module Refset' : CSig.SetS with type elt = global_reference
 module Refmap' : Map.S with type key = global_reference
 
-val safe_basename_of_global : global_reference -> identifier
+val safe_basename_of_global : global_reference -> Id.t
 
 (*s Warning and Error messages. *)
 
@@ -29,7 +30,7 @@ val error_inductive : global_reference -> 'a
 val error_nb_cons : unit -> 'a
 val error_module_clash : module_path -> module_path -> 'a
 val error_no_module_expr : module_path -> 'a
-val error_singleton_become_prop : identifier -> 'a
+val error_singleton_become_prop : Id.t -> 'a
 val error_unknown_module : qualid -> 'a
 val error_scheme : unit -> 'a
 val error_not_visible : global_reference -> 'a
@@ -37,7 +38,7 @@ val error_MPfile_as_mod : module_path -> bool -> 'a
 val check_inside_module : unit -> unit
 val check_inside_section : unit -> unit
 val check_loaded_modfile : module_path -> unit
-val msg_non_implicit : global_reference -> int -> name -> string
+val msg_non_implicit : global_reference -> int -> Name.t -> string
 val error_non_implicit : string -> 'a
 
 val info_file : string -> unit
@@ -45,10 +46,9 @@ val info_file : string -> unit
 (*s utilities about [module_path] and [kernel_names] and [global_reference] *)
 
 val occur_kn_in_ref : mutual_inductive -> global_reference -> bool
-val repr_of_r : global_reference -> module_path * dir_path * label
+val repr_of_r : global_reference -> module_path * DirPath.t * Label.t
 val modpath_of_r : global_reference -> module_path
-val label_of_r : global_reference -> label
-val current_toplevel : unit -> module_path
+val label_of_r : global_reference -> Label.t
 val base_mp : module_path -> module_path
 val is_modfile : module_path -> bool
 val string_of_modfile : module_path -> string
@@ -60,8 +60,8 @@ val mp_length : module_path -> int
 val prefixes_mp : module_path -> MPset.t
 val common_prefix_from_list :
   module_path -> module_path list -> module_path option
-val get_nth_label_mp : int -> module_path -> label
-val labels_of_ref : global_reference -> module_path * label list
+val get_nth_label_mp : int -> module_path -> Label.t
+val labels_of_ref : global_reference -> module_path * Label.t list
 
 (*s Some table-related operations *)
 
@@ -85,9 +85,10 @@ 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
 
-val add_projection : int -> constant -> unit
+val add_projection : int -> constant -> inductive -> unit
 val is_projection : global_reference -> bool
 val projection_arity : global_reference -> int
+val projection_info : global_reference -> inductive * int (* arity *)
 
 val add_info_axiom : global_reference -> unit
 val remove_info_axiom : global_reference -> unit
@@ -131,6 +132,14 @@ type opt_flag =
 
 val optims :  unit -> opt_flag
 
+(*s Controls whether dummy lambda are removed *)
+
+val conservative_types : unit -> bool
+
+(*s A comment to print at the beginning of the files *)
+
+val file_comment : unit -> string
+
 (*s Target language. *)
 
 type lang = Ocaml | Haskell | Scheme
@@ -162,7 +171,7 @@ val implicits_of_global : global_reference -> int list
 (*s Table for user-given custom ML extractions. *)
 
 (* UGLY HACK: registration of a function defined in [extraction.ml] *)
-val register_type_scheme_nb_args : (Environ.env -> Term.constr -> int) -> unit
+val type_scheme_nb_args_hook : (Environ.env -> Term.constr -> int) Hook.t
 
 val is_custom : global_reference -> bool
 val is_inline_custom : global_reference -> bool
@@ -176,7 +185,7 @@ val find_custom_match : ml_branch array -> string
 
 val extraction_language : lang -> unit
 val extraction_inline : bool -> reference list -> unit
-val print_extraction_inline : unit -> unit
+val print_extraction_inline : unit -> Pp.std_ppcmds
 val reset_extraction_inline : unit -> unit
 val extract_constant_inline :
   bool -> reference -> string list -> string -> unit
@@ -184,14 +193,14 @@ val extract_inductive :
   reference -> string -> string list -> string option -> unit
 
 
-type int_or_id = ArgInt of int | ArgId of identifier
+type int_or_id = ArgInt of int | ArgId of Id.t
 val extraction_implicit : reference -> int_or_id list -> unit
 
 (*s Table of blacklisted filenames *)
 
-val extraction_blacklist : identifier list -> unit
+val extraction_blacklist : Id.t list -> unit
 val reset_extraction_blacklist : unit -> unit
-val print_extraction_blacklist : unit -> unit
+val print_extraction_blacklist : unit -> Pp.std_ppcmds