Imported Upstream version 8.8.2upstream/8.8.2

42 files changed, 1214 insertions, 689 deletions

diff --git a/plugins/extraction/CHANGES b/plugins/extraction/CHANGES
index cf97ae3a..4bc3dba3 100644
--- a/plugins/extraction/CHANGES
+++ b/plugins/extraction/CHANGES
@@ -54,7 +54,7 @@ but also a few steps toward a more user-friendly extraction:
 
 * bug fixes: 
 - many concerning Records. 
-- a Stack Overflow with mutual inductive (PR#320)
+- a Stack Overflow with mutual inductive (BZ#320)
 - some optimizations have been removed since they were not type-safe:
   For example if e has type:  type 'x a = A
   Then:       match e with A -> A     -----X---->    e
@@ -125,7 +125,7 @@ but also a few steps toward a more user-friendly extraction:
 
   - the dummy constant "__" have changed. see README
 
-  - a few bug-fixes (#191 and others)
+  - a few bug-fixes (BZ#191 and others)
 
 7.2 -> 7.3
 
diff --git a/plugins/extraction/ExtrHaskellBasic.v b/plugins/extraction/ExtrHaskellBasic.v
index 294d6102..d08a81da 100644
--- a/plugins/extraction/ExtrHaskellBasic.v
+++ b/plugins/extraction/ExtrHaskellBasic.v
@@ -1,5 +1,7 @@
 (** Extraction to Haskell : use of basic Haskell types *)
 
+Require Coq.extraction.Extraction.
+
 Extract Inductive bool => "Prelude.Bool" [ "Prelude.True" "Prelude.False" ].
 Extract Inductive option => "Prelude.Maybe" [ "Prelude.Just" "Prelude.Nothing" ].
 Extract Inductive unit => "()" [ "()" ].
diff --git a/plugins/extraction/ExtrHaskellNatInt.v b/plugins/extraction/ExtrHaskellNatInt.v
index e94e7d42..267322d9 100644
--- a/plugins/extraction/ExtrHaskellNatInt.v
+++ b/plugins/extraction/ExtrHaskellNatInt.v
@@ -1,5 +1,7 @@
 (** Extraction of [nat] into Haskell's [Int] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Arith.
 Require Import ExtrHaskellNatNum.
 
diff --git a/plugins/extraction/ExtrHaskellNatInteger.v b/plugins/extraction/ExtrHaskellNatInteger.v
index 038f0ed8..4c5c71f5 100644
--- a/plugins/extraction/ExtrHaskellNatInteger.v
+++ b/plugins/extraction/ExtrHaskellNatInteger.v
@@ -1,5 +1,7 @@
 (** Extraction of [nat] into Haskell's [Integer] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Arith.
 Require Import ExtrHaskellNatNum.
 
diff --git a/plugins/extraction/ExtrHaskellNatNum.v b/plugins/extraction/ExtrHaskellNatNum.v
index 244eb85f..09b04446 100644
--- a/plugins/extraction/ExtrHaskellNatNum.v
+++ b/plugins/extraction/ExtrHaskellNatNum.v
@@ -6,6 +6,8 @@
  * implements [Num].
  *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Arith.
 Require Import EqNat.
 
@@ -32,4 +34,4 @@ Extract Constant Init.Nat.sub => "(\n m -> Prelude.max 0 (n Prelude.- m))".
 Extract Constant Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
 Extract Constant Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
 Extract Constant Init.Nat.div => "(\n m -> if m Prelude.== 0 then 0 else Prelude.div n m)".
-Extract Constant Init.Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
\ No newline at end of file
+Extract Constant Init.Nat.modulo => "(\n m -> if m Prelude.== 0 then 0 else Prelude.mod n m)".
diff --git a/plugins/extraction/ExtrHaskellString.v b/plugins/extraction/ExtrHaskellString.v
index 3558f4f2..ac1f6f91 100644
--- a/plugins/extraction/ExtrHaskellString.v
+++ b/plugins/extraction/ExtrHaskellString.v
@@ -2,6 +2,8 @@
  * Special handling of ascii and strings for extraction to Haskell.
  *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Ascii.
 Require Import String.
 
diff --git a/plugins/extraction/ExtrHaskellZInt.v b/plugins/extraction/ExtrHaskellZInt.v
index 66690851..0345ffc4 100644
--- a/plugins/extraction/ExtrHaskellZInt.v
+++ b/plugins/extraction/ExtrHaskellZInt.v
@@ -1,5 +1,7 @@
 (** Extraction of [Z] into Haskell's [Int] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import ZArith.
 Require Import ExtrHaskellZNum.
 
diff --git a/plugins/extraction/ExtrHaskellZInteger.v b/plugins/extraction/ExtrHaskellZInteger.v
index f192f16e..f7f9e2f8 100644
--- a/plugins/extraction/ExtrHaskellZInteger.v
+++ b/plugins/extraction/ExtrHaskellZInteger.v
@@ -1,5 +1,7 @@
 (** Extraction of [Z] into Haskell's [Integer] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import ZArith.
 Require Import ExtrHaskellZNum.
 
diff --git a/plugins/extraction/ExtrHaskellZNum.v b/plugins/extraction/ExtrHaskellZNum.v
index cbbfda75..4141bd20 100644
--- a/plugins/extraction/ExtrHaskellZNum.v
+++ b/plugins/extraction/ExtrHaskellZNum.v
@@ -6,6 +6,8 @@
  * implements [Num].
  *)
 
+Require Coq.extraction.Extraction.
+
 Require Import ZArith.
 Require Import EqNat.
 
diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v
index d9b000c2..36bb1148 100644
--- a/plugins/extraction/ExtrOcamlBasic.v
+++ b/plugins/extraction/ExtrOcamlBasic.v
@@ -1,11 +1,15 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+Require Coq.extraction.Extraction.
+
 (** Extraction to Ocaml : use of basic Ocaml types *)
 
 Extract Inductive bool => bool [ true false ].
diff --git a/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v
index c42938c8..2d832799 100644
--- a/plugins/extraction/ExtrOcamlBigIntConv.v
+++ b/plugins/extraction/ExtrOcamlBigIntConv.v
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** Extraction to Ocaml: conversion from/to [big_int] *)
@@ -13,6 +15,8 @@
     simplifies the use of [Big_int] (it can be found in the sources
     of Coq). *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Arith ZArith.
 
 Parameter bigint : Type.
diff --git a/plugins/extraction/ExtrOcamlIntConv.v b/plugins/extraction/ExtrOcamlIntConv.v
index 515fa52d..a3a4d45c 100644
--- a/plugins/extraction/ExtrOcamlIntConv.v
+++ b/plugins/extraction/ExtrOcamlIntConv.v
@@ -1,15 +1,19 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** Extraction to Ocaml: conversion from/to [int]
 
     Nota: no check that [int] values aren't generating overflows *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Arith ZArith.
 
 Parameter int : Type.
@@ -94,4 +98,4 @@ Extraction "/tmp/test.ml"
   pos_of_int int_of_pos
   z_of_int int_of_z
   n_of_int int_of_n.
-*)
\ No newline at end of file
+*)
diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v
index 3149e702..c403f7c5 100644
--- a/plugins/extraction/ExtrOcamlNatBigInt.v
+++ b/plugins/extraction/ExtrOcamlNatBigInt.v
@@ -1,13 +1,17 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** Extraction of [nat] into Ocaml's [big_int] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Arith Even Div2 EqNat Euclid.
 Require Import ExtrOcamlBasic.
 
@@ -42,7 +46,7 @@ Extract Constant EqNat.eq_nat_decide => "Big.eq".
 
 Extract Constant Peano_dec.eq_nat_dec => "Big.eq".
 
-Extract Constant Compare_dec.nat_compare =>
+Extract Constant Nat.compare =>
  "Big.compare_case Eq Lt Gt".
 
 Extract Constant Compare_dec.leb => "Big.le".
diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v
index 7c607f7a..a2f809a0 100644
--- a/plugins/extraction/ExtrOcamlNatInt.v
+++ b/plugins/extraction/ExtrOcamlNatInt.v
@@ -1,13 +1,17 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** Extraction of [nat] into Ocaml's [int] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Arith Even Div2 EqNat Euclid.
 Require Import ExtrOcamlBasic.
 
@@ -55,7 +59,7 @@ Extract Inlined Constant EqNat.eq_nat_decide => "(=)".
 
 Extract Inlined Constant Peano_dec.eq_nat_dec => "(=)".
 
-Extract Constant Compare_dec.nat_compare =>
+Extract Constant Nat.compare =>
  "fun n m -> if n=m then Eq else if n<m then Lt else Gt".
 Extract Inlined Constant Compare_dec.leb => "(<=)".
 Extract Inlined Constant Compare_dec.le_lt_dec => "(<=)".
diff --git a/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v
index 6af591ee..030b486b 100644
--- a/plugins/extraction/ExtrOcamlString.v
+++ b/plugins/extraction/ExtrOcamlString.v
@@ -1,13 +1,17 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (* Extraction to Ocaml : special handling of ascii and strings *)
 
+Require Coq.extraction.Extraction.
+
 Require Import Ascii String.
 
 Extract Inductive ascii => char
diff --git a/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v
index c9e8eac0..f7746b3e 100644
--- a/plugins/extraction/ExtrOcamlZBigInt.v
+++ b/plugins/extraction/ExtrOcamlZBigInt.v
@@ -1,13 +1,17 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** Extraction of [positive], [N] and [Z] into Ocaml's [big_int] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import ZArith NArith.
 Require Import ExtrOcamlBasic.
 
diff --git a/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v
index 4d33174b..f0e4b297 100644
--- a/plugins/extraction/ExtrOcamlZInt.v
+++ b/plugins/extraction/ExtrOcamlZInt.v
@@ -1,13 +1,17 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** Extraction of [positive], [N] and [Z] into Ocaml's [int] *)
 
+Require Coq.extraction.Extraction.
+
 Require Import ZArith NArith.
 Require Import ExtrOcamlBasic.
 
diff --git a/plugins/extraction/Extraction.v b/plugins/extraction/Extraction.v
new file mode 100644
index 00000000..b79d32e6
--- /dev/null
+++ b/plugins/extraction/Extraction.v
@@ -0,0 +1,11 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+Declare ML Module "extraction_plugin".
diff --git a/plugins/extraction/big.ml b/plugins/extraction/big.ml
index 44b81d76..9c0f373c 100644
--- a/plugins/extraction/big.ml
+++ b/plugins/extraction/big.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (** [Big] : a wrapper around ocaml [Big_int] with nicer names,
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 3c5f6cb7..f235bb89 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -1,14 +1,17 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Pp
 open Util
 open Names
+open ModPath
 open Namegen
 open Nameops
 open Libnames
@@ -44,7 +47,7 @@ let pp_apply2 st par args =
 
 let pr_binding = function
   | [] -> mt ()
-  | l  -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l
+  | l  -> str " " ++ prlist_with_sep (fun () -> str " ") Id.print l
 
 let pp_tuple_light f = function
   | [] -> mt ()
@@ -67,7 +70,9 @@ let pp_boxed_tuple f = function
     blocks is less that a line length. To avoid this awkward situation,
     we attach a big virtual size to [fnl] newlines. *)
 
-let fnl () = stras (1000000,"") ++ fnl ()
+(* EG: This looks quite suspicious... but beware of bugs *)
+(* let fnl () = stras (1000000,"") ++ fnl () *)
+let fnl () = fnl ()
 
 let fnl2 () = fnl () ++ fnl ()
 
@@ -91,10 +96,7 @@ let begins_with_CoqXX s =
 
 let unquote 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;
-    s
+  else String.map (fun c -> if c == '\'' then '~' else c) s
 
 let rec qualify delim = function
   | [] -> assert false
@@ -110,12 +112,17 @@ 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 (ascii_of_id id))
+[@@@ocaml.warning "-3"]       (* String.(un)capitalize_ascii since 4.03.0 GPR#124 *)
+let capitalize = String.capitalize
+let uncapitalize = String.uncapitalize
+[@@@ocaml.warning "+3"]
+
+let lowercase_id id = Id.of_string (uncapitalize (ascii_of_id id))
 let uppercase_id id =
   let s = ascii_of_id id in
   assert (not (String.is_empty s));
   if s.[0] == '_' then Id.of_string ("Coq_"^s)
-  else Id.of_string (String.capitalize s)
+  else Id.of_string (capitalize s)
 
 type kind = Term | Type | Cons | Mod
 
@@ -145,7 +152,7 @@ type env = Id.t list * Id.Set.t
 (*s Generic renaming issues for local variable names. *)
 
 let rec rename_id id avoid =
-  if Id.Set.mem id avoid then rename_id (lift_subscript id) avoid else id
+  if Id.Set.mem id avoid then rename_id (increment_subscript id) avoid else id
 
 let rec rename_vars avoid = function
   | [] ->
@@ -269,8 +276,8 @@ let params_ren_add, params_ren_mem =
   seen at this level.
 *)
 
-type visible_layer = { mp : module_path;
-		       params : module_path list;
+type visible_layer = { mp : ModPath.t;
+		       params : ModPath.t list;
 		       mutable content : Label.t KMap.t; }
 
 let pop_visible, push_visible, get_visible =
@@ -308,15 +315,16 @@ end
 
 module DupMap = Map.Make(DupOrd)
 
-let add_duplicate, check_duplicate =
+let add_duplicate, get_duplicate =
   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 := DupMap.add (mp,l) ren !dups
-  and check mp l = DupMap.find (mp, l) !dups
-  in (add,check)
+  and get mp l =
+    try Some (DupMap.find (mp, l) !dups) with Not_found -> None
+  in (add,get)
 
 type reset_kind = AllButExternal | Everything
 
@@ -399,7 +407,7 @@ let ref_renaming_fun (k,r) =
     let idg = safe_basename_of_global r in
     match l with
     | [""] -> (* this happens only at toplevel of the monolithic case *)
-      let globs = Id.Set.elements (get_global_ids ()) in
+      let globs = get_global_ids () in
       let id = next_ident_away (kindcase_id k idg) globs in
       Id.to_string id
     | _ -> modular_rename k idg
@@ -510,10 +518,11 @@ let pp_duplicate k' prefix mp rls olab =
       (* Here rls=s::rls', we search the label for s inside mp *)
       List.tl rls, get_nth_label_mp (mp_length mp - mp_length prefix) mp
   in
-  try dottify (check_duplicate prefix lbl :: rls')
-  with Not_found ->
-    assert (get_phase () == Pre); (* otherwise it's too late *)
-    add_duplicate prefix lbl; dottify rls
+  match get_duplicate prefix lbl with
+  | Some ren -> dottify (ren :: rls')
+  | None ->
+     assert (get_phase () == Pre); (* otherwise it's too late *)
+     add_duplicate prefix lbl; dottify rls
 
 let fstlev_ks k = function
   | [] -> assert false
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 2f560196..78545c8b 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -1,38 +1,39 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Names
 open Globnames
 open Miniml
-open Pp
 
 (** By default, in module Format, you can do horizontal placing of blocks
     even if they include newlines, as long as the number of chars in the
     blocks are less that a line length. To avoid this awkward situation,
     we attach a big virtual size to [fnl] newlines. *)
 
-val fnl : unit -> std_ppcmds
-val fnl2 : unit -> std_ppcmds
-val space_if : bool -> std_ppcmds
+val fnl : unit -> Pp.t
+val fnl2 : unit -> Pp.t
+val space_if : bool -> Pp.t
 
-val pp_par : bool -> std_ppcmds -> std_ppcmds
+val pp_par : bool -> Pp.t -> Pp.t
 
 (** [pp_apply] : a head part applied to arguments, possibly with parenthesis *)
-val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds
+val pp_apply : Pp.t -> bool -> Pp.t list -> Pp.t
 
 (** Same as [pp_apply], but with also protection of the head by parenthesis *)
-val pp_apply2 : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds
+val pp_apply2 : Pp.t -> bool -> Pp.t list -> Pp.t
 
-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 pp_tuple_light : (bool -> 'a -> Pp.t) -> 'a list -> Pp.t
+val pp_tuple : ('a -> Pp.t) -> 'a list -> Pp.t
+val pp_boxed_tuple : ('a -> Pp.t) -> 'a list -> Pp.t
 
-val pr_binding : Id.t list -> std_ppcmds
+val pr_binding : Id.t list -> Pp.t
 
 val rename_id : Id.t -> Id.Set.t -> Id.t
 
@@ -49,20 +50,20 @@ type phase = Pre | Impl | Intf
 val set_phase : phase -> unit
 val get_phase : unit -> phase
 
-val opened_libraries : unit -> module_path list
+val opened_libraries : unit -> ModPath.t list
 
 type kind = Term | Type | Cons | Mod
 
 val pp_global : kind -> global_reference -> string
-val pp_module : module_path -> string
+val pp_module : ModPath.t -> string
 
-val top_visible_mp : unit -> module_path
+val top_visible_mp : unit -> ModPath.t
 (* In [push_visible], the [module_path list] corresponds to
    module parameters, the innermost one coming first in the list *)
-val push_visible : module_path -> module_path list -> unit
+val push_visible : ModPath.t -> ModPath.t list -> unit
 val pop_visible : unit -> unit
 
-val check_duplicate : module_path -> Label.t -> string
+val get_duplicate : ModPath.t -> Label.t -> string option
 
 type reset_kind = AllButExternal | Everything
 
@@ -72,7 +73,7 @@ val set_keywords : Id.Set.t -> unit
 
 (** For instance: [mk_ind "Coq.Init.Datatypes" "nat"] *)
 
-val mk_ind : string -> string -> mutual_inductive
+val mk_ind : string -> string -> MutInd.t
 
 (** Special hack for constants of type Ascii.ascii : if an
     [Extract Inductive ascii => char] has been declared, then
@@ -80,4 +81,4 @@ val mk_ind : string -> string -> mutual_inductive
 
 val is_native_char : ml_ast -> bool
 val get_native_char : ml_ast -> char
-val pp_native_char : ml_ast -> std_ppcmds
+val pp_native_char : ml_ast -> Pp.t
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 52f22ee6..397cb292 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -1,15 +1,18 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Miniml
-open Term
+open Constr
 open Declarations
 open Names
+open ModPath
 open Libnames
 open Globnames
 open Pp
@@ -27,13 +30,13 @@ open Common
 let toplevel_env () =
   let get_reference = function
     | (_,kn), Lib.Leaf o ->
-	let mp,_,l = repr_kn kn in
+	let mp,_,l = KerName.repr kn in
 	begin match Libobject.object_tag o with
 	  | "CONSTANT" ->
-            let constant = Global.lookup_constant (constant_of_kn kn) in
+            let constant = Global.lookup_constant (Constant.make1 kn) in
             Some (l, SFBconst constant)
 	  | "INDUCTIVE" ->
-            let inductive = Global.lookup_mind (mind_of_kn kn) in
+            let inductive = Global.lookup_mind (MutInd.make1 kn) in
             Some (l, SFBmind inductive)
 	  | "MODULE" ->
             let modl = Global.lookup_module (MPdot (mp, l)) in
@@ -41,7 +44,7 @@ let toplevel_env () =
 	  | "MODULE TYPE" ->
             let modtype = Global.lookup_modtype (MPdot (mp, l)) in
             Some (l, SFBmodtype modtype)
-          | "INCLUDE" -> error "No extraction of toplevel Include yet."
+          | "INCLUDE" -> user_err Pp.(str "No extraction of toplevel Include yet.")
 	  | _ -> None
         end
     | _ -> None
@@ -72,21 +75,21 @@ module type VISIT = sig
 
   (* 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
+  val add_mp_all : ModPath.t -> unit
 
   (* Add reference / ... in the visit lists.
      These functions silently add the mp of their arg in the mp list *)
   val add_ref : global_reference -> unit
-  val add_kn : kernel_name -> unit
+  val add_kn : KerName.t -> unit
   val add_decl_deps : ml_decl -> unit
   val add_spec_deps : ml_spec -> unit
 
   (* Test functions:
      is a particular object a needed dependency for the current extraction ? *)
-  val needed_ind : mutual_inductive -> bool
-  val needed_cst : constant -> bool
-  val needed_mp : module_path -> bool
-  val needed_mp_all : module_path -> bool
+  val needed_ind : MutInd.t -> bool
+  val needed_cst : Constant.t -> bool
+  val needed_mp : ModPath.t -> bool
+  val needed_mp_all : ModPath.t -> bool
 end
 
 module Visit : VISIT = struct
@@ -101,8 +104,8 @@ module Visit : VISIT = struct
     v.kn <- KNset.empty;
     v.mp <- MPset.empty;
     v.mp_all <- MPset.empty
-  let needed_ind i = KNset.mem (user_mind i) v.kn
-  let needed_cst c = KNset.mem (user_con c) v.kn
+  let needed_ind i = KNset.mem (MutInd.user i) v.kn
+  let needed_cst c = KNset.mem (Constant.user c) v.kn
   let needed_mp mp = MPset.mem mp v.mp || MPset.mem mp v.mp_all
   let needed_mp_all mp = MPset.mem mp v.mp_all
   let add_mp mp =
@@ -111,10 +114,10 @@ module Visit : VISIT = struct
     check_loaded_modfile mp;
     v.mp <- MPset.union (prefixes_mp mp) v.mp;
     v.mp_all <- MPset.add mp v.mp_all
-  let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (modpath kn)
+  let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (KerName.modpath kn)
   let add_ref = function
-    | ConstRef c -> add_kn (user_con c)
-    | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_kn (user_mind ind)
+    | ConstRef c -> add_kn (Constant.user c)
+    | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_kn (MutInd.user ind)
     | VarRef _ -> assert false
   let add_decl_deps = decl_iter_references add_ref add_ref add_ref
   let add_spec_deps = spec_iter_references add_ref add_ref add_ref
@@ -131,25 +134,28 @@ let rec add_labels mp = function
 exception Impossible
 
 let check_arity env cb =
-  let t = Typeops.type_of_constant_type env cb.const_type in
+  let t = cb.const_type in
   if Reduction.is_arity env t then raise Impossible
 
-let check_fix env cb i =
+let get_body lbody =
+  EConstr.of_constr (Mod_subst.force_constr lbody)
+
+let check_fix env sg cb i =
   match cb.const_body with
     | Def lbody ->
-	(match kind_of_term (Mod_subst.force_constr lbody) with
-	  | Fix ((_,j),recd) when Int.equal i j -> check_arity env cb; (true,recd)
+        (match EConstr.kind sg (get_body 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) =
+let prec_declaration_equal sg (na1, ca1, ta1) (na2, ca2, ta2) =
   Array.equal Name.equal na1 na2 &&
-  Array.equal eq_constr ca1 ca2 &&
-  Array.equal eq_constr ta1 ta2
+  Array.equal (EConstr.eq_constr sg) ca1 ca2 &&
+  Array.equal (EConstr.eq_constr sg) ta1 ta2
 
-let factor_fix env l cb msb =
-  let _,recd as check = check_fix env cb 0 in
+let factor_fix env sg l cb msb =
+  let _,recd as check = check_fix env sg cb 0 in
   let n = Array.length (let fi,_,_ = recd in fi) in
   if Int.equal n 1 then [|l|], recd, msb
   else begin
@@ -160,9 +166,9 @@ let factor_fix env l cb msb =
       (fun j ->
 	 function
 	   | (l,SFBconst cb') ->
-	       let check' = check_fix env cb' (j+1) in
-	       if not ((fst check : bool) == (fst check') &&
-		   prec_declaration_equal (snd check) (snd check'))
+              let check' = check_fix env sg cb' (j+1) in
+              if not ((fst check : bool) == (fst check') &&
+                        prec_declaration_equal sg (snd check) (snd check'))
 	       then raise Impossible;
 	       labels.(j+1) <- l;
 	   | _ -> raise Impossible) msb';
@@ -174,26 +180,32 @@ let factor_fix env l cb msb =
     (hack proposed by Elie)
 *)
 
-let expand_mexpr env mp me =
+let expand_mexpr env mpo me =
   let inl = Some (Flags.get_inline_level()) in
-  Mod_typing.translate_mse env (Some mp) inl me
-
-(** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def].
-    To check with Elie. *)
+  Mod_typing.translate_mse env mpo inl me
 
-let rec mp_of_mexpr = function
-  | MEident mp -> mp
-  | MEwith (seb,_) -> mp_of_mexpr seb
-  | _ -> assert false
+let expand_modtype env mp me =
+  let inl = Some (Flags.get_inline_level()) in
+  Mod_typing.translate_modtype env mp inl ([],me)
 
 let no_delta = Mod_subst.empty_delta_resolver
 
-let env_for_mtb_with_def env mp me idl =
+let flatten_modtype env mp me_alg struc_opt =
+  match struc_opt with
+  | Some me -> me, no_delta
+  | None ->
+     let mtb = expand_modtype env mp me_alg in
+     mtb.mod_type, mtb.mod_delta
+
+(** Ad-hoc update of environment, inspired by [Mod_typing.check_with_aux_def].
+*)
+
+let env_for_mtb_with_def env mp me reso 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 no_delta env
+  Modops.add_structure mp before reso env
 
 let make_cst resolver mp l =
   Mod_subst.constant_of_delta_kn resolver (KerName.make2 mp l)
@@ -233,20 +245,26 @@ let rec extract_structure_spec env mp reso = function
    [extract_mexpression_spec] should come from a [mod_type_alg] field.
    This way, any encountered [MEident] should be a true module type. *)
 
-and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with
+and extract_mexpr_spec env mp1 (me_struct_o,me_alg) = match me_alg with
   | MEident mp -> Visit.add_mp_all mp; MTident mp
   | MEwith(me',WithDef(idl,(c,ctx)))->
-      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 *)
+      let me_struct,delta = flatten_modtype env mp1 me' me_struct_o in
+      let env' = env_for_mtb_with_def env mp1 me_struct delta idl in
+      let mt = extract_mexpr_spec env mp1 (None,me') in
+      let sg = Evd.from_env env in
+      (match extract_with_type env' sg (EConstr.of_constr c) with
+       (* cb may contain some kn *)
 	 | None -> mt
-	 | Some (vl,typ) -> MTwith(mt,ML_With_type(idl,vl,typ)))
+	 | Some (vl,typ) ->
+            type_iter_references Visit.add_ref typ;
+            MTwith(mt,ML_With_type(idl,vl,typ)))
   | MEwith(me',WithMod(idl,mp))->
       Visit.add_mp_all mp;
-      MTwith(extract_mexpr_spec env mp1 (me_struct,me'), ML_With_module(idl,mp))
+      MTwith(extract_mexpr_spec env mp1 (None,me'), ML_With_module(idl,mp))
   | MEapply _ ->
      (* No higher-order module type in OCaml : we use the expanded version *)
-     extract_msignature_spec env mp1 no_delta (*TODO*) me_struct
+     let me_struct,delta = flatten_modtype env mp1 me_alg me_struct_o in
+     extract_msignature_spec env mp1 delta me_struct
 
 and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with
   | MoreFunctor (mbid, mtb, me_alg') ->
@@ -257,8 +275,8 @@ and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with
       let mp = MPbound mbid in
       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)
+                extract_mexpression_spec env' mp1 (me_struct',me_alg'))
+  | NoFunctor m -> extract_mexpr_spec env mp1 (Some me_struct,m)
 
 and extract_msignature_spec env mp1 reso = function
   | NoFunctor struc ->
@@ -270,7 +288,8 @@ and extract_msignature_spec env mp1 reso = function
       MTfunsig (mbid, extract_mbody_spec env mp mtb,
 		extract_msignature_spec env' mp1 reso me)
 
-and extract_mbody_spec env mp mb = match mb.mod_type_alg with
+and extract_mbody_spec : 'a. _ -> _ -> 'a generic_module_body -> _ =
+  fun 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_delta mb.mod_type
 
@@ -285,12 +304,13 @@ let rec extract_structure env mp reso ~all = function
   | [] -> []
   | (l,SFBconst cb) :: struc ->
       (try
-	 let vl,recd,struc = factor_fix env l cb struc in
+         let sg = Evd.from_env env in
+         let vl,recd,struc = factor_fix env sg l cb struc in
 	 let vc = Array.map (make_cst reso mp) vl in
 	 let ms = extract_structure env mp reso ~all struc in
 	 let b = Array.exists Visit.needed_cst vc in
 	 if all || b then
-	   let d = extract_fixpoint env vc recd in
+           let d = extract_fixpoint env sg 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
@@ -330,11 +350,11 @@ let rec extract_structure env mp reso ~all = function
 
 and extract_mexpr env mp = function
   | MEwith _ -> assert false (* no 'with' syntax for modules *)
-  | me when lang () != Ocaml ->
+  | me when lang () != Ocaml || Table.is_extrcompute () ->
       (* In Haskell/Scheme, we expand everything.
          For now, we also extract everything, dead code will be removed later
          (see [Modutil.optimize_struct]. *)
-      let sign,_,delta,_ = expand_mexpr env mp me in
+      let sign,_,delta,_ = expand_mexpr env (Some mp) me in
       extract_msignature env mp delta ~all:true sign
   | MEident mp ->
       if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false;
@@ -435,7 +455,7 @@ let mono_filename f =
 	  else
             try Id.of_string (Filename.basename f)
 	    with UserError _ ->
-              error "Extraction: provided filename is not a valid identifier"
+              user_err Pp.(str "Extraction: provided filename is not a valid identifier")
 	in
 	Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id
 
@@ -472,13 +492,14 @@ let formatter dry file =
     if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ())
     else
       match file with
-	| Some f -> Pp_control.with_output_to f
+	| Some f -> Topfmt.with_output_to f
 	| None -> Format.formatter_of_buffer buf
   in
+  (* XXX: Fixme, this shouldn't depend on Topfmt *)
   (* We never want to see ellipsis ... in extracted code *)
   Format.pp_set_max_boxes ft max_int;
   (* We reuse the width information given via "Set Printing Width" *)
-  (match Pp_control.get_margin () with
+  (match Topfmt.get_margin () with
     | None -> ()
     | Some i ->
       Format.pp_set_margin ft i;
@@ -507,8 +528,7 @@ let print_structure_to_file (fn,si,mo) dry struc =
   in
   (* First, a dry run, for computing objects to rename or duplicate *)
   set_phase Pre;
-  let devnull = formatter true None in
-  pp_with devnull (d.pp_struct struc);
+  ignore (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
@@ -519,8 +539,10 @@ let print_structure_to_file (fn,si,mo) dry struc =
     set_phase Impl;
     pp_with ft (d.preamble mo comment opened unsafe_needs);
     pp_with ft (d.pp_struct struc);
+    Format.pp_print_flush ft ();
     Option.iter close_out cout;
   with reraise ->
+    Format.pp_print_flush ft ();
     Option.iter close_out cout; raise reraise
   end;
   if not dry then Option.iter info_file fn;
@@ -533,8 +555,10 @@ let print_structure_to_file (fn,si,mo) dry struc =
 	 set_phase Intf;
 	 pp_with ft (d.sig_preamble mo comment opened unsafe_needs);
 	 pp_with ft (d.pp_sig (signature_of_structure struc));
+         Format.pp_print_flush ft ();
 	 close_out cout;
        with reraise ->
+         Format.pp_print_flush ft ();
 	 close_out cout; raise reraise
        end;
        info_file si)
@@ -554,11 +578,12 @@ let print_structure_to_file (fn,si,mo) dry struc =
 let reset () =
   Visit.reset (); reset_tables (); reset_renaming_tables Everything
 
-let init modular library =
-  check_inside_section (); check_inside_module ();
+let init ?(compute=false) ?(inner=false) modular library =
+  if not inner then (check_inside_section (); check_inside_module ());
   set_keywords (descr ()).keywords;
   set_modular modular;
   set_library library;
+  set_extrcompute compute;
   reset ();
   if modular && lang () == Scheme then error_scheme ()
 
@@ -572,8 +597,8 @@ let warns () =
 let rec locate_ref = function
   | [] -> [],[]
   | r::l ->
-      let q = snd (qualid_of_reference r) in
-      let mpo = try Some (Nametab.locate_module q) with Not_found -> None
+      let q = qualid_of_reference r in
+      let mpo = try Some (Nametab.locate_module q.CAst.v) with Not_found -> None
       and ro =
         try Some (Smartlocate.global_with_alias r)
         with Nametab.GlobalizationError _ | UserError _ -> None
@@ -583,7 +608,7 @@ let rec locate_ref = function
 	| None, Some r -> let refs,mps = locate_ref l in r::refs,mps
 	| Some mp, None -> let refs,mps = locate_ref l in refs,mp::mps
 	| Some mp, Some r ->
-           warning_ambiguous_name (q,mp,r);
+           warning_ambiguous_name (q.CAst.v,mp,r);
            let refs,mps = locate_ref l in refs,mp::mps
 
 (*s Recursive extraction in the Coq toplevel. The vernacular command is
@@ -621,7 +646,7 @@ let separate_extraction lr =
     is \verb!Extraction! [qualid]. *)
 
 let simple_extraction r =
-  Vernacentries.dump_global (Misctypes.AN r);
+  Vernacentries.dump_global CAst.(make (Misctypes.AN r));
   match locate_ref [r] with
   | ([], [mp]) as p -> full_extr None p
   | [r],[] ->
@@ -653,7 +678,7 @@ let extraction_library is_rec m =
   let l = List.rev (environment_until (Some dir_m)) in
   let select l (mp,struc) =
     if Visit.needed_mp mp
-    then (mp, extract_structure env mp no_delta true struc) :: l
+    then (mp, extract_structure env mp no_delta ~all:true struc) :: l
     else l
   in
   let struc = List.fold_left select [] l in
@@ -668,15 +693,76 @@ let extraction_library is_rec m =
   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
+(** For extraction compute, we flatten all the module structure,
+    getting rid of module types or unapplied functors *)
+
+let flatten_structure struc =
+  let rec flatten_elem (lab,elem) = match elem with
+    |SEdecl d -> [d]
+    |SEmodtype _ -> []
+    |SEmodule m -> match m.ml_mod_expr with
+      |MEfunctor _ -> []
+      |MEident _ | MEapply _ -> assert false (* should be expanded *)
+      |MEstruct (_,elems) -> flatten_elems elems
+  and flatten_elems l = List.flatten (List.map flatten_elem l)
+  in flatten_elems (List.flatten (List.map snd struc))
+
+let structure_for_compute env sg c =
+  init false false ~compute:true;
+  let ast, mlt = Extraction.extract_constr env sg 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
+  (flatten_structure struc), ast, mlt
+
+(* For the test-suite :
+   extraction to a temporary file + run ocamlc on it *)
+
+let compile f =
+  try
+    let args = ["ocamlc";"-I";Filename.dirname f;"-c";f^"i";f] in
+    let res = CUnix.sys_command (Envars.ocamlfind ()) args in
+    match res with
+    | Unix.WEXITED 0 -> ()
+    | Unix.WEXITED n | Unix.WSIGNALED n | Unix.WSTOPPED n ->
+       CErrors.user_err
+         Pp.(str "Compilation of file " ++ str f ++
+             str " failed with exit code " ++ int n)
+  with Unix.Unix_error (e,_,_) ->
+    CErrors.user_err
+      Pp.(str "Compilation of file " ++ str f ++
+          str " failed with error " ++ str (Unix.error_message e))
+
+let remove f =
+  if Sys.file_exists f then Sys.remove f
+
+let extract_and_compile l =
+  if lang () != Ocaml then
+    CErrors.user_err (Pp.str "This command only works with OCaml extraction");
+  let f = Filename.temp_file "testextraction" ".ml" in
+  let () = full_extraction (Some f) l in
+  let () = compile f in
+  let () = remove f; remove (f^"i") in
+  let base = Filename.chop_suffix f ".ml" in
+  let () = remove (base^".cmo"); remove (base^".cmi") in
+  Feedback.msg_notice (str "Extracted code successfully compiled")
+
+(* Show the extraction of the current ongoing proof *)
+
+let show_extraction () =
+  init ~inner:true false false;
+  let prf = Proof_global.give_me_the_proof () in
+  let sigma, env = Pfedit.get_current_context () in
+  let trms = Proof.partial_proof prf in
+  let extr_term t =
+    let ast, ty = extract_constr env sigma t in
+    let mp = Lib.current_mp () in
+    let l = Label.of_id (Proof_global.get_current_proof_name ()) in
+    let fake_ref = ConstRef (Constant.make2 mp l) in
+    let decl = Dterm (fake_ref, ast, ty) in
+    print_one_decl [] mp decl
+  in
+  Feedback.msg_notice (Pp.prlist_with_sep Pp.fnl extr_term trms)
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 90f4f911..591d3bb8 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*s This module declares the extraction commands. *)
@@ -17,18 +19,26 @@ val full_extraction : string option -> reference list -> unit
 val separate_extraction : reference list -> unit
 val extraction_library : bool -> Id.t -> unit
 
+(* For the test-suite : extraction to a temporary file + ocamlc on it *)
+
+val extract_and_compile : reference list -> unit
+
 (* For debug / external output via coqtop.byte + Drop : *)
 
 val mono_environment :
- global_reference list -> module_path list -> Miniml.ml_structure
+ global_reference list -> ModPath.t list -> Miniml.ml_structure
 
 (* Used by the Relation Extraction plugin *)
 
 val print_one_decl :
-  Miniml.ml_structure -> module_path -> Miniml.ml_decl -> Pp.std_ppcmds
+  Miniml.ml_structure -> ModPath.t -> Miniml.ml_decl -> Pp.t
 
 (* Used by Extraction Compute *)
 
 val structure_for_compute :
-  Term.constr ->
-    Miniml.ml_flat_structure * Miniml.ml_ast * Miniml.ml_type
+  Environ.env -> Evd.evar_map -> EConstr.t ->
+    Miniml.ml_decl list * Miniml.ml_ast * Miniml.ml_type
+
+(* Show the extraction of the current ongoing proof *)
+
+val show_extraction : unit -> unit
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index a980a43f..f25f6362 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -1,16 +1,18 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*i*)
 open Util
 open Names
 open Term
-open Vars
+open Constr
 open Declarations
 open Declareops
 open Environ
@@ -31,22 +33,20 @@ open Context.Rel.Declaration
 exception I of inductive_kind
 
 (* A set of all fixpoint functions currently being extracted *)
-let current_fixpoints = ref ([] : constant list)
-
-let none = Evd.empty
+let current_fixpoints = ref ([] : Constant.t list)
 
 (* NB: In OCaml, [type_of] and [get_of] might raise
    [SingletonInductiveBecomeProp]. This exception will be caught
    in late wrappers around the exported functions of this file,
    in order to display the location of the issue. *)
 
-let type_of env c =
+let type_of env sg c =
   let polyprop = (lang() == Haskell) in
-  Retyping.get_type_of ~polyprop env none (strip_outer_cast c)
+  Retyping.get_type_of ~polyprop env sg (strip_outer_cast sg c)
 
-let sort_of env c =
+let sort_of env sg c =
   let polyprop = (lang() == Haskell) in
-  Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c)
+  Retyping.get_sort_family_of ~polyprop env sg (strip_outer_cast sg c)
 
 (*S Generation of flags and signatures. *)
 
@@ -73,49 +73,88 @@ 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 : flag =
-  let t = whd_all env none t in
-  match kind_of_term t with
-    | Prod (x,t,c) -> flag_of_type (push_rel (LocalAssum (x,t)) env) c
-    | Sort s when Sorts.is_prop s -> (Logic,TypeScheme)
+let rec flag_of_type env sg t : flag =
+  let t = whd_all env sg t in
+  match EConstr.kind sg t with
+    | Prod (x,t,c) -> flag_of_type (EConstr.push_rel (LocalAssum (x,t)) env) sg c
+    | Sort s when Sorts.is_prop (EConstr.ESorts.kind sg s) -> (Logic,TypeScheme)
     | Sort _ -> (Info,TypeScheme)
-    | _ -> if (sort_of env t) == InProp then (Logic,Default) else (Info,Default)
+    | _ -> if (sort_of env sg t) == InProp then (Logic,Default) else (Info,Default)
 
 (*s Two particular cases of [flag_of_type]. *)
 
-let is_default env t = match flag_of_type env t with
+let is_default env sg t = match flag_of_type env sg t with
 | (Info, Default) -> true
 | _ -> false
 
 exception NotDefault of kill_reason
 
-let check_default env t =
-  match flag_of_type env t with
+let check_default env sg t =
+  match flag_of_type env sg t with
     | _,TypeScheme -> raise (NotDefault Ktype)
     | Logic,_ -> raise (NotDefault Kprop)
     | _ -> ()
 
-let is_info_scheme env t = match flag_of_type env t with
+let is_info_scheme env sg t = match flag_of_type env sg t with
 | (Info, TypeScheme) -> true
 | _ -> false
 
+let push_rel_assum (n, t) env =
+  EConstr.push_rel (LocalAssum (n, t)) env
+
+let push_rels_assum assums =
+  EConstr.push_rel_context (List.map (fun (x,t) -> LocalAssum (x,t)) assums)
+
+let get_body lconstr = EConstr.of_constr (Mod_subst.force_constr lconstr)
+
+let get_opaque env c =
+  EConstr.of_constr
+    (Opaqueproof.force_proof (Environ.opaque_tables env) c)
+
+let applistc c args = EConstr.mkApp (c, Array.of_list args)
+
+(* Same as [Environ.push_rec_types], but for [EConstr.t] *)
+let push_rec_types (lna,typarray,_) env =
+  let ctxt =
+    Array.map2_i
+      (fun i na t -> LocalAssum (na, EConstr.Vars.lift i t)) lna typarray
+  in
+  Array.fold_left (fun e assum -> EConstr.push_rel assum e) env ctxt
+
+(* Same as [Termops.nb_lam], but for [EConstr.t] *)
+let nb_lam sg c = List.length (fst (EConstr.decompose_lam sg c))
+
+(* Same as [Term.decompose_lam_n] but for [EConstr.t] *)
+let decompose_lam_n sg n =
+  let rec lamdec_rec l n c =
+    if n <= 0 then l,c
+    else match EConstr.kind sg c with
+      | Lambda (x,t,c) -> lamdec_rec ((x,t)::l) (n-1) c
+      | Cast (c,_,_)     -> lamdec_rec l n c
+      | _ -> raise Not_found
+  in
+  lamdec_rec [] n
+
 (*s [type_sign] gernerates a signature aimed at treating a type application. *)
 
-let rec type_sign env c =
-  match kind_of_term (whd_all env none c) with
+let rec type_sign env sg c =
+  match EConstr.kind sg (whd_all env sg c) with
     | Prod (n,t,d) ->
-	(if is_info_scheme env t then Keep else Kill Kprop)
-	:: (type_sign (push_rel_assum (n,t) env) d)
+        (if is_info_scheme env sg t then Keep else Kill Kprop)
+        :: (type_sign (push_rel_assum (n,t) env) sg d)
     | _ -> []
 
-let rec type_scheme_nb_args env c =
-  match kind_of_term (whd_all env none c) with
+let rec type_scheme_nb_args env sg c =
+  match EConstr.kind sg (whd_all env sg c) with
     | Prod (n,t,d) ->
-	let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in
-	if is_info_scheme env t then n+1 else n
+        let n = type_scheme_nb_args (push_rel_assum (n,t) env) sg d in
+        if is_info_scheme env sg t then n+1 else n
     | _ -> 0
 
-let _ = Hook.set type_scheme_nb_args_hook type_scheme_nb_args
+let type_scheme_nb_args' env c =
+  type_scheme_nb_args env (Evd.from_env env) (EConstr.of_constr c)
+
+let _ = Hook.set type_scheme_nb_args_hook type_scheme_nb_args'
 
 (*s [type_sign_vl] does the same, plus a type var list. *)
 
@@ -132,21 +171,22 @@ let make_typvar n vl =
     if not (String.contains s '\'') && Unicode.is_basic_ascii s then id
     else id_of_name Anonymous
   in
+  let vl = Id.Set.of_list vl in
   next_ident_away id' vl
 
-let rec type_sign_vl env c =
-  match kind_of_term (whd_all env none c) with
+let rec type_sign_vl env sg c =
+  match EConstr.kind sg (whd_all env sg 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 Kprop::s, vl
-	else Keep::s, (make_typvar n vl) :: vl
+        let s,vl = type_sign_vl (push_rel_assum (n,t) env) sg d in
+        if not (is_info_scheme env sg t) then Kill Kprop::s, vl
+        else Keep::s, (make_typvar n vl) :: vl
     | _ -> [],[]
 
-let rec nb_default_params env c =
-  match kind_of_term (whd_all env none c) with
+let rec nb_default_params env sg c =
+  match EConstr.kind sg (whd_all env sg c) with
     | Prod (n,t,d) ->
-	let n = nb_default_params (push_rel_assum (n,t) env) d in
-	if is_default env t then n+1 else n
+        let n = nb_default_params (push_rel_assum (n,t) env) sg d in
+        if is_default env sg t then n+1 else n
     | _ -> 0
 
 (* Enriching a signature with implicit information *)
@@ -197,7 +237,7 @@ let parse_ind_args si args relmax =
     | [] -> Int.Map.empty
     | Kill _ :: s -> parse (i+1) j s
     | Keep :: s ->
-      (match kind_of_term args.(i-1) with
+      (match Constr.kind args.(i-1) with
 	 | 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
@@ -213,62 +253,62 @@ let parse_ind_args si args relmax =
    generate ML type var anymore (in subterms for example). *)
 
 
-let rec extract_type env db j c args =
-  match kind_of_term (whd_betaiotazeta Evd.empty c) with
+let rec extract_type env sg db j c args =
+  match EConstr.kind sg (whd_betaiotazeta sg c) with
     | App (d, args') ->
-	(* We just accumulate the arguments. *)
-	extract_type env db j d (Array.to_list args' @ args)
+        (* We just accumulate the arguments. *)
+        extract_type env sg db j d (Array.to_list args' @ args)
     | Lambda (_,_,d) ->
 	(match args with
 	   | [] -> assert false (* A lambda cannot be a type. *)
-	   | a :: args -> extract_type env db j (subst1 a d) args)
+           | a :: args -> extract_type env sg db j (EConstr.Vars.subst1 a d) args)
     | Prod (n,t,d) ->
 	assert (List.is_empty args);
 	let env' = push_rel_assum (n,t) env in
-	(match flag_of_type env t with
+        (match flag_of_type env sg t with
 	   | (Info, Default) ->
 	       (* Standard case: two [extract_type] ... *)
-	       let mld = extract_type env' (0::db) j d [] in
+               let mld = extract_type env' sg (0::db) j d [] in
 	       (match expand env mld with
 		  | Tdummy d -> Tdummy d
-		  | _ -> Tarr (extract_type env db 0 t [], mld))
+                  | _ -> Tarr (extract_type env sg db 0 t [], mld))
 	   | (Info, TypeScheme) when j > 0 ->
 	       (* A new type var. *)
-	       let mld = extract_type env' (j::db) (j+1) d [] in
+               let mld = extract_type env' sg (j::db) (j+1) d [] in
 	       (match expand env mld with
 		  | Tdummy d -> Tdummy d
 		  | _ -> Tarr (Tdummy Ktype, mld))
 	   | _,lvl ->
-	       let mld = extract_type env' (0::db) j d [] in
+               let mld = extract_type env' sg (0::db) j d [] in
 	       (match expand env mld with
 		  | Tdummy d -> Tdummy d
 		  | _ ->
 		      let reason = if lvl == TypeScheme then Ktype else Kprop in
 		      Tarr (Tdummy reason, mld)))
     | Sort _ -> Tdummy Ktype (* The two logical cases. *)
-    | _ when sort_of env (applist (c, args)) == InProp -> Tdummy Kprop
+    | _ when sort_of env sg (applistc c args) == InProp -> Tdummy Kprop
     | Rel n ->
-	(match lookup_rel n env with
-           | LocalDef (_,t,_) -> extract_type env db j (lift n t) args
+        (match EConstr.lookup_rel n env with
+           | LocalDef (_,t,_) ->
+               extract_type env sg db j (EConstr.Vars.lift n t) args
 	   | _ ->
 	       (* Asks [db] a translation for [n]. *)
 	       if n > List.length db then Tunknown
 	       else let n' = List.nth db (n-1) in
 	       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 env c in
-	(match flag_of_type env typ with
+    | Const (kn,u) ->
+        let r = ConstRef kn in
+        let typ = type_of env sg (EConstr.mkConstU (kn,u)) in
+        (match flag_of_type env sg typ with
 	   | (Logic,_) -> assert false (* Cf. logical cases above *)
 	   | (Info, TypeScheme) ->
-	       let mlt = extract_type_app env db (r, type_sign env typ) args in
-	       (match cb.const_body with
+               let mlt = extract_type_app env sg db (r, type_sign env sg typ) args in
+               (match (lookup_constant kn env).const_body with
 		  | Undef _ | OpaqueDef _ -> mlt
-		  | Def _ when is_custom r -> mlt
+                  | Def _ when is_custom (ConstRef kn) -> mlt
 		  | Def lbody ->
-		      let newc = applist (Mod_subst.force_constr lbody, args) in
-		      let mlt' = extract_type env db j newc [] in
+                      let newc = applistc (get_body lbody) args in
+                      let mlt' = extract_type env sg 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 *)
@@ -277,32 +317,51 @@ let rec extract_type env db j c args =
 		      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
+               (match (lookup_constant kn env).const_body with
 		  | Undef _  | OpaqueDef _ -> Tunknown (* Brutal approx ... *)
 		  | Def lbody ->
 		      (* We try to reduce. *)
-		      let newc = applist (Mod_subst.force_constr lbody, args) in
-		      extract_type env db j newc []))
+                      let newc = applistc (get_body lbody) args in
+                      extract_type env sg db j newc []))
     | 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 _ | Proj _ -> Tunknown
-    | _ -> assert false
+        let s = (extract_ind env kn).ind_packets.(i).ip_sign in
+        extract_type_app env sg db (IndRef (kn,i),s) args
+    | Proj (p,t) ->
+       (* Let's try to reduce, if it hasn't already been done. *)
+       if Projection.unfolded p then Tunknown
+       else
+         extract_type env sg db j (EConstr.mkProj (Projection.unfold p, t)) args
+    | Case _ | Fix _ | CoFix _ -> Tunknown
+    | Evar _ | Meta _ -> Taxiom (* only possible during Show Extraction *)
+    | Var v ->
+       (* For Show Extraction *)
+       let open Context.Named.Declaration in
+       (match EConstr.lookup_named v env with
+        | LocalDef (_,body,_) ->
+           extract_type env sg db j (EConstr.applist (body,args)) []
+        | LocalAssum (_,ty) ->
+           let r = VarRef v in
+           (match flag_of_type env sg ty with
+            | (Logic,_) -> assert false (* Cf. logical cases above *)
+            | (Info, TypeScheme) ->
+              extract_type_app env sg db (r, type_sign env sg ty) args
+            | (Info, Default) -> Tunknown))
+    | Cast _ | LetIn _ | Construct _ -> assert false
 
 (*s Auxiliary function dealing with type application.
   Precondition: [r] is a type scheme represented by the signature [s],
   and is completely applied: [List.length args = List.length s]. *)
 
-and extract_type_app env db (r,s) args =
+and extract_type_app env sg db (r,s) args =
   let ml_args =
     List.fold_right
       (fun (b,c) a -> if b == Keep then
-	 let p = List.length (fst (splay_prod env none (type_of env c))) in
+         let p = List.length (fst (splay_prod env sg (type_of env sg c))) in
          let db = iterate (fun l -> 0 :: l) p db in
-         (extract_type_scheme env db c p) :: a
+         (extract_type_scheme env sg db c p) :: a
        else a)
       (List.combine s args) []
-  in Tglob (r,  ml_args)
+  in Tglob (r, ml_args)
 
 (*S Extraction of a type scheme. *)
 
@@ -313,18 +372,18 @@ 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 Int.equal p 0 then extract_type env db 0 c []
+and extract_type_scheme env sg db c p =
+  if Int.equal p 0 then extract_type env sg db 0 c []
   else
-    let c = whd_betaiotazeta Evd.empty c in
-    match kind_of_term c with
+    let c = whd_betaiotazeta sg c in
+    match EConstr.kind sg c with
       | Lambda (n,t,d) ->
-          extract_type_scheme (push_rel_assum (n,t) env) db d (p-1)
+          extract_type_scheme (push_rel_assum (n,t) env) sg db d (p-1)
       | _ ->
-          let rels = fst (splay_prod env none (type_of env c)) in
+          let rels = fst (splay_prod env sg (type_of env sg c)) in
           let env = push_rels_assum rels env in
-          let eta_args = List.rev_map mkRel (List.interval 1 p) in
-          extract_type env db 0 (lift p c) eta_args
+          let eta_args = List.rev_map EConstr.mkRel (List.interval 1 p) in
+          extract_type env sg db 0 (EConstr.Vars.lift p c) eta_args
 
 
 (*S Extraction of an inductive type. *)
@@ -351,14 +410,14 @@ and extract_really_ind env kn mib =
        (cf Vector and bug #2570) *)
     let equiv =
       if lang () != Ocaml ||
-	 (not (modular ()) && at_toplevel (mind_modpath kn)) ||
-	 KerName.equal (canonical_mind kn) (user_mind kn)
+	 (not (modular ()) && at_toplevel (MutInd.modpath kn)) ||
+	 KerName.equal (MutInd.canonical kn) (MutInd.user kn)
       then
 	NoEquiv
       else
 	begin
-	  ignore (extract_ind env (mind_of_kn (canonical_mind kn)));
-	  Equiv (canonical_mind kn)
+	  ignore (extract_ind env (MutInd.make1 (MutInd.canonical kn)));
+	  Equiv (MutInd.canonical kn)
 	end
     in
     (* Everything concerning parameters. *)
@@ -366,6 +425,7 @@ and extract_really_ind env kn mib =
     let mip0 = mib.mind_packets.(0) in
     let npar = mib.mind_nparams in
     let epar = push_rel_context mib.mind_params_ctxt env in
+    let sg = Evd.from_env env in
     (* First pass: we store inductive signatures together with *)
     (* their type var list. *)
     let packets =
@@ -373,8 +433,9 @@ and extract_really_ind env kn mib =
 	(fun i mip ->
 	   let (_,u),_ = 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 ar = EConstr.of_constr ar in
+           let info = (fst (flag_of_type env sg ar) = Info) in
+           let s,v = if info then type_sign_vl env sg ar else [],[] in
 	   let t = Array.make (Array.length mip.mind_nf_lc) [] in
 	   { ip_typename = mip.mind_typename;
 	     ip_consnames = mip.mind_consnames;
@@ -400,13 +461,14 @@ and extract_really_ind env kn mib =
 	  let t = snd (decompose_prod_n npar types.(j)) in
 	  let prods,head = dest_prod epar t in
 	  let nprods = List.length prods in
-          let args = match kind_of_term head with
-            | App (f,args) -> args (* [kind_of_term f = Ind ip] *)
+          let args = match Constr.kind head with
+            | App (f,args) -> args (* [Constr.kind f = Ind ip] *)
             | _ -> [||]
           in
 	  let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in
 	  let db = db_from_ind dbmap npar in
-	  p.ip_types.(j) <- extract_type_cons epar db dbmap t (npar+1)
+          p.ip_types.(j) <-
+            extract_type_cons epar sg db dbmap (EConstr.of_constr t) (npar+1)
 	done
     done;
     (* Third pass: we determine special cases. *)
@@ -415,7 +477,7 @@ and extract_really_ind env kn mib =
 	let ip = (kn, 0) in
 	let r = IndRef ip in
 	if is_custom r then raise (I Standard);
-	if mib.mind_finite == Decl_kinds.CoFinite then raise (I Coinductive);
+        if mib.mind_finite == 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);
@@ -429,7 +491,7 @@ and extract_really_ind env kn mib =
 	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
+	let rec names_prod t = match Constr.kind t with
 	  | Prod(n,_,t) -> n::(names_prod t)
 	  | LetIn(_,_,_,t) -> names_prod t
 	  | Cast(t,_,_) -> names_prod t
@@ -459,10 +521,9 @@ and extract_really_ind env kn mib =
 	(* Is this record officially declared with its projections ? *)
 	(* If so, we use this information. *)
 	begin try
-	  let n = nb_default_params env
-            (Inductive.type_of_inductive env ((mib,mip0),u))
-	  in
-	  let check_proj kn = if Cset.mem kn !projs then add_projection n kn ip
+          let ty = Inductive.type_of_inductive env ((mib,mip0),u) in
+          let n = nb_default_params env sg (EConstr.of_constr ty) 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 -> ()
@@ -487,13 +548,13 @@ and extract_really_ind env kn mib =
    - [i] is the rank of the current product (initially [params_nb+1])
 *)
 
-and extract_type_cons env db dbmap c i =
-  match kind_of_term (whd_all env none c) with
+and extract_type_cons env sg db dbmap c i =
+  match EConstr.kind sg (whd_all env sg c) with
     | Prod (n,t,d) ->
 	let env' = push_rel_assum (n,t) env 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
+        let l = extract_type_cons env' sg db' dbmap d (i+1) in
+        (extract_type env sg db 0 t []) :: l
     | _ -> []
 
 (*s Recording the ML type abbreviation of a Coq type scheme constant. *)
@@ -508,16 +569,17 @@ and mlt_env env r = match r with
         match lookup_typedef kn cb with
         | Some _ as o -> o
         | None ->
-           let typ = Typeops.type_of_constant_type env cb.const_type
+           let sg = Evd.from_env env in
+           let typ = EConstr.of_constr cb.const_type
            (* FIXME not sure if we should instantiate univs here *) in
-	   match flag_of_type env typ with
-	   | Info,TypeScheme ->
-	      let body = Mod_subst.force_constr l_body in
-	      let s = type_sign env typ in
-	      let db = db_from_sign s in
-	      let t = extract_type_scheme env db body (List.length s)
-	      in add_typedef kn cb t; Some t
-	   | _ -> None
+           match flag_of_type env sg typ with
+           | Info,TypeScheme ->
+              let body = get_body l_body in
+              let s = type_sign env sg typ in
+              let db = db_from_sign s in
+              let t = extract_type_scheme env sg db body (List.length s)
+              in add_typedef kn cb t; Some t
+           | _ -> None
 
 and expand env = type_expand (mlt_env env)
 and type2signature env = type_to_signature (mlt_env env)
@@ -527,16 +589,16 @@ let type_expunge_from_sign env = type_expunge_from_sign (mlt_env env)
 
 (*s Extraction of the type of a constant. *)
 
-let record_constant_type env kn opt_typ =
+let record_constant_type env sg kn opt_typ =
   let cb = lookup_constant kn env in
   match lookup_cst_type kn cb with
   | Some schema -> schema
   | None ->
      let typ = match opt_typ with
-       | None -> Typeops.type_of_constant_type env cb.const_type
+       | None -> EConstr.of_constr cb.const_type
        | Some typ -> typ
      in
-     let mlt = extract_type env [] 1 typ [] in
+     let mlt = extract_type env sg [] 1 typ [] in
      let schema = (type_maxvar mlt, mlt) in
      let () = add_cst_type kn cb schema in
      schema
@@ -548,74 +610,86 @@ let record_constant_type env kn opt_typ =
 (* [mle] is a ML environment [Mlenv.t]. *)
 (* [mlt] is the ML type we want our extraction of [(c args)] to have. *)
 
-let rec extract_term env mle mlt c args =
-  match kind_of_term c with
+let rec extract_term env sg mle mlt c args =
+  match EConstr.kind sg c with
     | App (f,a) ->
-	extract_term env mle mlt f (Array.to_list a @ args)
+       extract_term env sg mle mlt f (Array.to_list a @ args)
     | Lambda (n, t, d) ->
 	let id = id_of_name n in
 	(match args with
 	   | a :: l ->
 	       (* We make as many [LetIn] as possible. *)
- 	       let d' = mkLetIn (Name id,a,t,applistc d (List.map (lift 1) l))
-	       in extract_term env mle mlt d' []
+               let l' = List.map (EConstr.Vars.lift 1) l in
+               let d' = EConstr.mkLetIn (Name id,a,t,applistc d l') in
+               extract_term env sg mle mlt d' []
 	   | [] ->
 	       let env' = push_rel_assum (Name id, t) env in
 	       let id, a =
-		 try check_default env t; Id id, new_meta()
-		 with NotDefault d -> Dummy, Tdummy d
+                 try check_default env sg t; Id id, new_meta()
+                 with NotDefault d -> Dummy, Tdummy d
 	       in
 	       let b = new_meta () in
 	       (* If [mlt] cannot be unified with an arrow type, then magic! *)
 	       let magic = needs_magic (mlt, Tarr (a, b)) in
-	       let d' = extract_term env' (Mlenv.push_type mle a) b d [] in
+               let d' = extract_term env' sg (Mlenv.push_type mle a) b d [] in
 	       put_magic_if magic (MLlam (id, d')))
     | LetIn (n, c1, t1, c2) ->
 	let id = id_of_name n in
-	let env' = push_rel (LocalDef (Name id, c1, t1)) env in
+        let env' = EConstr.push_rel (LocalDef (Name id, c1, t1)) env in
 	(* We directly push the args inside the [LetIn].
            TODO: the opt_let_app flag is supposed to prevent that *)
-	let args' = List.map (lift 1) args in
+        let args' = List.map (EConstr.Vars.lift 1) args in
 	(try
-	  check_default env t1;
+          check_default env sg t1;
 	  let a = new_meta () in
-	  let c1' = extract_term env mle a c1 [] in
+          let c1' = extract_term env sg mle a c1 [] in
 	  (* The type of [c1'] is generalized and stored in [mle]. *)
 	  let mle' =
 	    if generalizable c1'
 	    then Mlenv.push_gen mle a
 	    else Mlenv.push_type mle a
 	  in
-	  MLletin (Id id, c1', extract_term env' mle' mlt c2 args')
+          MLletin (Id id, c1', extract_term env' sg mle' mlt c2 args')
 	with NotDefault d ->
 	  let mle' = Mlenv.push_std_type mle (Tdummy d) in
-	  ast_pop (extract_term env' mle' mlt c2 args'))
+          ast_pop (extract_term env' sg mle' mlt c2 args'))
     | Const (kn,_) ->
-	extract_cst_app env mle mlt kn args
+        extract_cst_app env sg mle mlt kn args
     | Construct (cp,_) ->
-	extract_cons_app env mle mlt cp args
+        extract_cons_app env sg mle mlt cp args
     | Proj (p, c) ->
         let term = Retyping.expand_projection env (Evd.from_env env) p c [] in
-	  extract_term env mle mlt term args
+        extract_term env sg mle mlt term 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]. *)
 	let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n)
-	in extract_app env mle mlt extract_rel args
+        in extract_app env sg mle mlt extract_rel args
     | Case ({ci_ind=ip},_,c0,br) ->
- 	extract_app env mle mlt (extract_case env mle (ip,c0,br)) args
+        extract_app env sg mle mlt (extract_case env sg mle (ip,c0,br)) args
     | Fix ((_,i),recd) ->
- 	extract_app env mle mlt (extract_fix env mle i recd) args
+        extract_app env sg mle mlt (extract_fix env sg mle i recd) args
     | CoFix (i,recd) ->
- 	extract_app env mle mlt (extract_fix env mle i recd) args
-    | Cast (c,_,_) -> extract_term env mle mlt c args
-    | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ | Var _ -> assert false
+        extract_app env sg mle mlt (extract_fix env sg mle i recd) args
+    | Cast (c,_,_) -> extract_term env sg mle mlt c args
+    | Evar _ | Meta _ -> MLaxiom
+    | Var v ->
+       (* Only during Show Extraction *)
+       let open Context.Named.Declaration in
+       let ty = match EConstr.lookup_named v env with
+         | LocalAssum (_,ty) -> ty
+         | LocalDef (_,_,ty) -> ty
+       in
+       let vty = extract_type env sg [] 0 ty [] in
+       let extract_var mlt = put_magic (mlt,vty) (MLglob (VarRef v)) in
+       extract_app env sg mle mlt extract_var args
+    | Ind _ | Prod _ | Sort _ -> assert false
 
 (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *)
 
-and extract_maybe_term env mle mlt c =
-  try check_default env (type_of env c);
-    extract_term env mle mlt c []
+and extract_maybe_term env sg mle mlt c =
+  try check_default env sg (type_of env sg c);
+    extract_term env sg mle mlt c []
   with NotDefault d ->
     put_magic (mlt, Tdummy d) (MLdummy d)
 
@@ -625,28 +699,28 @@ and extract_maybe_term env mle mlt c =
    This gives us the expected type of the head. Then we use the
    [mk_head] to produce the ML head from this type. *)
 
-and extract_app env mle mlt mk_head args =
+and extract_app env sg mle mlt mk_head args =
   let metas = List.map new_meta args in
   let type_head = type_recomp (metas, mlt) in
-  let mlargs = List.map2 (extract_maybe_term env mle) metas args in
+  let mlargs = List.map2 (extract_maybe_term env sg mle) metas args in
   mlapp (mk_head type_head) mlargs
 
 (*s Auxiliary function used to extract arguments of constant or constructor. *)
 
-and make_mlargs env e s args typs =
+and make_mlargs env sg e s args typs =
   let rec f = function
     | [], [], _ -> []
-    | a::la, t::lt, [] -> extract_maybe_term env e t a :: (f (la,lt,[]))
-    | a::la, t::lt, Keep::s -> extract_maybe_term env e t a :: (f (la,lt,s))
+    | a::la, t::lt, [] -> extract_maybe_term env sg e t a :: (f (la,lt,[]))
+    | a::la, t::lt, Keep::s -> extract_maybe_term env sg e t a :: (f (la,lt,s))
     | _::la, _::lt, _::s -> f (la,lt,s)
     | _ -> assert false
   in f (args,typs,s)
 
 (*s Extraction of a constant applied to arguments. *)
 
-and extract_cst_app env mle mlt kn args =
+and extract_cst_app env sg mle mlt kn args =
   (* First, the [ml_schema] of the constant, in expanded version. *)
-  let nb,t = record_constant_type env kn None in
+  let nb,t = record_constant_type env sg 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. *)
@@ -672,7 +746,7 @@ and extract_cst_app env mle mlt kn args =
   let ls = List.length s in
   let la = List.length args in
   (* The ml arguments, already expunged from known logical ones *)
-  let mla = make_mlargs env mle s args metas in
+  let mla = make_mlargs env sg mle s args metas in
   let mla =
     if magic1 || lang () != Ocaml then mla
     else
@@ -717,7 +791,7 @@ 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 sg mle mlt (((kn,i) as ip,j) as cp) 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
@@ -758,7 +832,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
     put_magic_if magic2
       (dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la))
   else
-    let mla = make_mlargs env mle s args' metas in
+    let mla = make_mlargs env sg mle s args' metas in
     if Int.equal la (ls + params_nb)
     then put_magic_if (magic2 && not magic1) (head mla)
     else (* [ params_nb <= la <= ls + params_nb ] *)
@@ -769,7 +843,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
 
 (*S Extraction of a case. *)
 
-and extract_case env mle ((kn,i) as ip,c,br) mlt =
+and extract_case env sg 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 = constructors_nrealargs_env env ip in
@@ -780,9 +854,9 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
     MLexn "absurd case"
   end else
     (* [c] has an inductive type, and is not a type scheme type. *)
-    let t = type_of env c in
+    let t = type_of env sg c in
     (* The only non-informative case: [c] is of sort [Prop] *)
-    if (sort_of env t) == InProp then
+    if (sort_of env sg t) == InProp then
       begin
 	add_recursors env kn; (* May have passed unseen if logical ... *)
 	(* Logical singleton case: *)
@@ -790,7 +864,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	assert (Int.equal br_size 1);
 	let s = iterate (fun l -> Kill Kprop :: l) ni.(0) [] in
 	let mlt = iterate (fun t -> Tarr (Tdummy Kprop, t)) ni.(0) mlt in
-	let e = extract_maybe_term env mle mlt br.(0) in
+        let e = extract_maybe_term env sg mle mlt br.(0) in
 	snd (case_expunge s e)
       end
     else
@@ -799,7 +873,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
       let metas = Array.init (List.length oi.ip_vars) new_meta in
       (* The extraction of the head. *)
       let type_head = Tglob (IndRef ip, Array.to_list metas) in
-      let a = extract_term env mle type_head c [] in
+      let a = extract_term env sg mle type_head c [] in
       (* The extraction of each branch. *)
       let extract_branch i =
 	let r = ConstructRef (ip,i+1) in
@@ -810,7 +884,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 	let s = List.map (type2sign env) oi.ip_types.(i) in
 	let s = sign_with_implicits r s mi.ind_nparams in
 	(* Extraction of the branch (in functional form). *)
-	let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in
+        let e = extract_maybe_term env sg mle (type_recomp (l,mlt)) br.(i) in
 	(* We suppress dummy arguments according to signature. *)
 	let ids,e = case_expunge s e in
 	(List.rev ids, Pusual r, e)
@@ -832,12 +906,12 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
 
 (*s Extraction of a (co)-fixpoint. *)
 
-and extract_fix env mle i (fi,ti,ci as recd) mlt =
+and extract_fix env sg mle i (fi,ti,ci as recd) mlt =
   let env = push_rec_types recd env in
   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 sg mle) metas ci in
   MLfix (i, Array.map id_of_name fi, ei)
 
 (*S ML declarations. *)
@@ -845,34 +919,34 @@ 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 decomp_lams_eta_n n m env c t =
-  let rels = fst (splay_prod_n env none n t) in
+let decomp_lams_eta_n n m env sg c t =
+  let rels = fst (splay_prod_n env sg n t) in
   let rels = List.map (fun (LocalAssum (id,c) | LocalDef (id,_,c)) -> (id,c)) rels in
-  let rels',c = decompose_lam c in
+  let rels',c = EConstr.decompose_lam sg 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 (List.interval 1 d) in
-  rels, applist (lift d c,eta_args)
+  let eta_args = List.rev_map EConstr.mkRel (List.interval 1 d) in
+  rels, applistc (EConstr.Vars.lift d c) eta_args
 
 (* Let's try to identify some situation where extracted code
    will allow generalisation of type variables *)
 
-let rec gentypvar_ok c = match kind_of_term c with
+let rec gentypvar_ok sg c = match EConstr.kind sg c with
   | Lambda _ | Const _ -> true
   | 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
-  | Cast (c,_,_) -> gentypvar_ok c
+      Array.for_all (EConstr.isRel sg) v && gentypvar_ok sg c
+  | Cast (c,_,_) -> gentypvar_ok sg c
   | _ -> false
 
 (*s From a constant to a ML declaration. *)
 
-let extract_std_constant env kn body typ =
+let extract_std_constant env sg kn body typ =
   reset_meta_count ();
   (* The short type [t] (i.e. possibly with abbreviations). *)
-  let t = snd (record_constant_type env kn (Some typ)) in
+  let t = snd (record_constant_type env sg kn (Some typ)) in
   (* The real type [t']: without head products, expanded, *)
   (* and with [Tvar] translated to [Tvar'] (not instantiable). *)
   let l,t' = type_decomp (expand env (var2var' t)) in
@@ -887,14 +961,14 @@ let extract_std_constant env kn body typ =
      break user's clever let-ins and partial applications). *)
   let rels, c =
     let n = List.length s
-    and m = nb_lam body in
-    if n <= m then decompose_lam_n n body
+    and m = nb_lam sg body in
+    if n <= m then decompose_lam_n sg n body
     else
       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
+      then decompose_lam_n sg m body
+      else decomp_lams_eta_n n m env sg body typ
   in
   (* Should we do one eta-expansion to avoid non-generalizable '_a ? *)
   let rels, c =
@@ -902,9 +976,9 @@ let extract_std_constant env kn body typ =
     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)
+    if lang () == Ocaml && empty_s && not (gentypvar_ok sg c)
       && not (List.is_empty s') && not (Int.equal (type_maxvar t) 0)
-    then decomp_lams_eta_n (n+1) n env body typ
+    then decomp_lams_eta_n (n+1) n env sg body typ
     else rels,c
   in
   let n = List.length rels in
@@ -918,16 +992,16 @@ let extract_std_constant env kn body typ =
   (* The according Coq environment. *)
   let env = push_rels_assum rels env in
   (* The real extraction: *)
-  let e = extract_term env mle t' c [] in
+  let e = extract_term env sg mle t' c [] in
   (* Expunging term and type from dummy lambdas. *)
   let trm = term_expunge s (ids,e) in
   trm, type_expunge_from_sign env s t
 
 (* Extracts the type of an axiom, honors the Extraction Implicit declaration. *)
-let extract_axiom env kn typ =
+let extract_axiom env sg kn typ =
   reset_meta_count ();
   (* The short type [t] (i.e. possibly with abbreviations). *)
-  let t = snd (record_constant_type env kn (Some typ)) in
+  let t = snd (record_constant_type env sg kn (Some typ)) in
   (* The real type [t']: without head products, expanded, *)
   (* and with [Tvar] translated to [Tvar'] (not instantiable). *)
   let l,_ = type_decomp (expand env (var2var' t)) in
@@ -936,18 +1010,19 @@ let extract_axiom env kn typ =
   let s = sign_with_implicits (ConstRef kn) s 0 in
   type_expunge_from_sign env s t
 
-let extract_fixpoint env vkn (fi,ti,ci) =
+let extract_fixpoint env sg vkn (fi,ti,ci) =
   let n = Array.length vkn in
   let types = Array.make n (Tdummy Kprop)
   and terms = Array.make n (MLdummy Kprop) in
   let kns = Array.to_list vkn in
   current_fixpoints := kns;
   (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *)
-  let sub = List.rev_map mkConst kns in
+  let sub = List.rev_map EConstr.mkConst kns in
   for i = 0 to n-1 do
-    if sort_of env ti.(i) != InProp then
+    if sort_of env sg ti.(i) != InProp then
       try
-        let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in
+        let e,t = extract_std_constant env sg vkn.(i)
+                   (EConstr.Vars.substl sub ci.(i)) ti.(i) in
         terms.(i) <- e;
         types.(i) <- t;
       with SingletonInductiveBecomesProp id ->
@@ -957,32 +1032,33 @@ let extract_fixpoint env vkn (fi,ti,ci) =
   Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types)
 
 let extract_constant env kn cb =
+  let sg = Evd.from_env env in
   let r = ConstRef kn in
-  let typ = Typeops.type_of_constant_type env cb.const_type in
+  let typ = EConstr.of_constr cb.const_type in
   let warn_info () = if not (is_custom r) then add_info_axiom r in
   let warn_log () = if not (constant_has_body cb) then add_log_axiom r
   in
   let mk_typ_ax () =
-    let n = type_scheme_nb_args env typ in
+    let n = type_scheme_nb_args env sg typ in
     let ids = iterate (fun l -> anonymous_name::l) n [] in
     Dtype (r, ids, Taxiom)
   in
   let mk_typ c =
-    let s,vl = type_sign_vl env typ in
+    let s,vl = type_sign_vl env sg typ in
     let db = db_from_sign s in
-    let t = extract_type_scheme env db c (List.length s)
+    let t = extract_type_scheme env sg db c (List.length s)
     in Dtype (r, vl, t)
   in
   let mk_ax () =
-    let t = extract_axiom env kn typ in
+    let t = extract_axiom env sg kn typ in
     Dterm (r, MLaxiom, t)
   in
   let mk_def c =
-    let e,t = extract_std_constant env kn c typ in
+    let e,t = extract_std_constant env sg kn c typ in
     Dterm (r,e,t)
   in
   try
-    match flag_of_type env typ with
+    match flag_of_type env sg typ with
     | (Logic,TypeScheme) -> warn_log (); Dtype (r, [], Tdummy Ktype)
     | (Logic,Default) -> warn_log (); Dterm (r, MLdummy Kprop, Tdummy Kprop)
     | (Info,TypeScheme) ->
@@ -990,73 +1066,72 @@ let extract_constant env kn cb =
 	  | Undef _ -> warn_info (); mk_typ_ax ()
 	  | Def c ->
 	     (match cb.const_proj with
-	      | None -> mk_typ (Mod_subst.force_constr c)
-	      | Some pb -> mk_typ pb.proj_body)
+              | None -> mk_typ (get_body c)
+              | Some pb -> mk_typ (EConstr.of_constr pb.proj_body))
 	  | OpaqueDef c ->
 	    add_opaque r;
-	    if access_opaque () then
-              mk_typ (Opaqueproof.force_proof (Environ.opaque_tables env) c)
+            if access_opaque () then mk_typ (get_opaque env c)
             else mk_typ_ax ())
     | (Info,Default) ->
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_ax ()
 	  | Def c ->
 	     (match cb.const_proj with
-	      | None -> mk_def (Mod_subst.force_constr c)
-	      | Some pb -> mk_def pb.proj_body)
+              | None -> mk_def (get_body c)
+              | Some pb -> mk_def (EConstr.of_constr pb.proj_body))
 	  | OpaqueDef c ->
 	    add_opaque r;
-	    if access_opaque () then
-              mk_def (Opaqueproof.force_proof (Environ.opaque_tables env) c)
+            if access_opaque () then mk_def (get_opaque env c)
             else mk_ax ())
   with SingletonInductiveBecomesProp id ->
     error_singleton_become_prop id (Some (ConstRef kn))
 
 let extract_constant_spec env kn cb =
+  let sg = Evd.from_env env in
   let r = ConstRef kn in
-  let typ = Typeops.type_of_constant_type env cb.const_type in
+  let typ = EConstr.of_constr cb.const_type in
   try
-    match flag_of_type env typ with
+    match flag_of_type env sg typ with
     | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype))
     | (Logic, Default) -> Sval (r, Tdummy Kprop)
     | (Info, TypeScheme) ->
-	let s,vl = type_sign_vl env typ in
+        let s,vl = type_sign_vl env sg typ in
 	(match cb.const_body with
 	  | Undef _ | OpaqueDef _ -> Stype (r, vl, None)
 	  | Def body ->
 	      let db = db_from_sign s in
-              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))
+              let body = get_body body in
+              let t = extract_type_scheme env sg 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 t = snd (record_constant_type env sg kn (Some typ)) in
+        Sval (r, type_expunge env t)
   with SingletonInductiveBecomesProp id ->
     error_singleton_become_prop id (Some (ConstRef kn))
 
-let extract_with_type env c =
+let extract_with_type env sg c =
   try
-    let typ = type_of env c in
-    match flag_of_type env typ with
+    let typ = type_of env sg c in
+    match flag_of_type env sg typ with
     | (Info, TypeScheme) ->
-	let s,vl = type_sign_vl env typ in
-	let db = db_from_sign s in
-	let t = extract_type_scheme env db c (List.length s) in
-	Some (vl, t)
+        let s,vl = type_sign_vl env sg typ in
+        let db = db_from_sign s in
+        let t = extract_type_scheme env sg db c (List.length s) in
+        Some (vl, t)
     | _ -> None
   with SingletonInductiveBecomesProp id ->
     error_singleton_become_prop id None
 
-let extract_constr env c =
+let extract_constr env sg c =
   reset_meta_count ();
   try
-    let typ = type_of env c in
-    match flag_of_type env typ with
+    let typ = type_of env sg c in
+    match flag_of_type env sg typ with
     | (_,TypeScheme) -> MLdummy Ktype, Tdummy Ktype
     | (Logic,_) -> MLdummy Kprop, Tdummy Kprop
     | (Info,Default) ->
-       let mlt = extract_type env [] 1 typ [] in
-       extract_term env Mlenv.empty mlt c [], mlt
+       let mlt = extract_type env sg [] 1 typ [] in
+       extract_term env sg Mlenv.empty mlt c [], mlt
   with SingletonInductiveBecomesProp id ->
     error_singleton_become_prop id None
 
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index cdda777a..d27c79cb 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -1,35 +1,39 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*s Extraction from Coq terms to Miniml. *)
 
 open Names
-open Term
 open Declarations
 open Environ
+open Evd
 open Miniml
 
-val extract_constant : env -> constant -> constant_body -> ml_decl
+val extract_constant : env -> Constant.t -> constant_body -> ml_decl
 
-val extract_constant_spec : env -> constant -> constant_body -> ml_spec
+val extract_constant_spec : env -> Constant.t -> constant_body -> ml_spec
 
 (** For extracting "module ... with ..." declaration *)
 
-val extract_with_type : env -> constr -> ( Id.t list * ml_type ) option
+val extract_with_type :
+  env -> evar_map -> EConstr.t -> ( Id.t list * ml_type ) option
 
 val extract_fixpoint :
-  env -> constant array -> (constr, types) prec_declaration -> ml_decl
+  env -> evar_map -> Constant.t array ->
+    (EConstr.t, EConstr.types) Constr.prec_declaration -> ml_decl
 
-val extract_inductive : env -> mutual_inductive -> ml_ind
+val extract_inductive : env -> MutInd.t -> ml_ind
 
-(** For extraction compute *)
+(** For Extraction Compute and Show Extraction *)
 
-val extract_constr : env -> constr -> ml_ast * ml_type
+val extract_constr : env -> evar_map -> EConstr.t -> ml_ast * ml_type
 
 (*s Is a [ml_decl] or a [ml_spec] logical ? *)
 
diff --git a/plugins/extraction/extraction_plugin.mlpack b/plugins/extraction/extraction_plugin.mlpack
index 9184f650..7f98348e 100644
--- a/plugins/extraction/extraction_plugin.mlpack
+++ b/plugins/extraction/extraction_plugin.mlpack
@@ -1,3 +1,4 @@
+Miniml
 Table
 Mlutil
 Modutil
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 19fda4ae..93909f3e 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -1,24 +1,24 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(*i camlp4deps: "grammar/grammar.cma" i*)
+open Pcoq.Prim
 
 DECLARE PLUGIN "extraction_plugin"
 
 (* ML names *)
 
+open Ltac_plugin
 open Genarg
 open Stdarg
-open Constrarg
-open Pcoq.Prim
 open Pp
 open Names
-open Nameops
 open Table
 open Extract_env
 
@@ -33,7 +33,7 @@ END
 
 let pr_int_or_id _ _ _ = function
   | ArgInt i -> int i
-  | ArgId id -> pr_id id
+  | ArgId id -> Id.print id
 
 ARGUMENT EXTEND int_or_id
   PRINTED BY pr_int_or_id
@@ -42,14 +42,20 @@ ARGUMENT EXTEND int_or_id
 END
 
 let pr_language = function
-  | Ocaml -> str "Ocaml"
+  | Ocaml -> str "OCaml"
   | Haskell -> str "Haskell"
   | Scheme -> str "Scheme"
   | JSON -> str "JSON"
 
+let warn_deprecated_ocaml_spelling =
+  CWarnings.create ~name:"deprecated-ocaml-spelling" ~category:"deprecated"
+    (fun () ->
+      strbrk ("The spelling \"OCaml\" should be used instead of \"Ocaml\"."))
+
 VERNAC ARGUMENT EXTEND language
 PRINTED BY pr_language
-| [ "Ocaml" ] -> [ Ocaml ]
+| [ "Ocaml" ] -> [ let _ = warn_deprecated_ocaml_spelling () in Ocaml ]
+| [ "OCaml" ] -> [ Ocaml ]
 | [ "Haskell" ] -> [ Haskell ]
 | [ "Scheme" ] -> [ Scheme ]
 | [ "JSON" ] -> [ JSON ]
@@ -65,6 +71,10 @@ VERNAC COMMAND EXTEND Extraction CLASSIFIED AS QUERY
 (* Monolithic extraction to a file *)
 | [ "Extraction" string(f) ne_global_list(l) ]
   -> [ full_extraction (Some f) l ]
+
+(* Extraction to a temporary file and OCaml compilation *)
+| [ "Extraction" "TestCompile" ne_global_list(l) ]
+  -> [ extract_and_compile l ]
 END
 
 VERNAC COMMAND EXTEND SeparateExtraction CLASSIFIED AS QUERY
@@ -150,3 +160,9 @@ VERNAC COMMAND EXTEND ExtractionInductive CLASSIFIED AS SIDEFF
     mlname(id) "[" mlname_list(idl) "]" string_opt(o) ]
   -> [ extract_inductive x id idl o ]
 END
+(* Show the extraction of the current proof *)
+
+VERNAC COMMAND EXTEND ShowExtraction CLASSIFIED AS QUERY
+| [ "Show" "Extraction" ]
+  -> [ show_extraction () ]
+END
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 0692c88c..e6234c14 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*s Production of Haskell syntax. *)
@@ -12,7 +14,6 @@ open Pp
 open CErrors
 open Util
 open Names
-open Nameops
 open Globnames
 open Table
 open Miniml
@@ -20,9 +21,10 @@ open Mlutil
 open Common
 
 (*s Haskell renaming issues. *)
-
+[@@@ocaml.warning "-3"]       (* String.(un)capitalize_ascii since 4.03.0 GPR#124 *)
 let pr_lower_id id = str (String.uncapitalize (Id.to_string id))
 let pr_upper_id id = str (String.capitalize (Id.to_string id))
+[@@@ocaml.warning "+3"]
 
 let keywords =
   List.fold_right (fun s -> Id.Set.add (Id.of_string s))
@@ -58,7 +60,6 @@ let preamble mod_name comment used_modules usf =
    else
      str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++
      str "import qualified GHC.Base" ++ fnl () ++
-     str "import qualified GHC.Prim" ++ fnl () ++
      str "#else" ++ fnl () ++
      str "-- HUGS" ++ fnl () ++
      str "import qualified IOExts" ++ fnl () ++
@@ -78,7 +79,7 @@ let preamble mod_name comment used_modules usf =
   (if not usf.tunknown then mt ()
    else
      str "#ifdef __GLASGOW_HASKELL__" ++ fnl () ++
-     str "type Any = GHC.Prim.Any" ++ fnl () ++
+     str "type Any = GHC.Base.Any" ++ fnl () ++
      str "#else" ++ fnl () ++
      str "-- HUGS" ++ fnl () ++
      str "type Any = ()" ++ fnl () ++
@@ -92,7 +93,7 @@ let preamble mod_name comment used_modules usf =
 let pp_abst = function
   | [] -> (mt ())
   | l  -> (str "\\" ++
-             prlist_with_sep (fun () -> (str " ")) pr_id l ++
+             prlist_with_sep (fun () -> (str " ")) Id.print l ++
              str " ->" ++ spc ())
 
 (*s The pretty-printer for haskell syntax *)
@@ -108,7 +109,7 @@ 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))
+      (try Id.print (List.nth vl (pred i))
        with Failure _ -> (str "a" ++ int i))
     | Tglob (r,[]) -> pp_global Type r
     | Tglob (IndRef(kn,0),l)
@@ -145,9 +146,9 @@ let rec pp_expr par env args =
     | MLrel n ->
 	let id = get_db_name n env in
         (* Try to survive to the occurrence of a Dummy rel.
-           TODO: we should get rid of this hack (cf. #592) *)
+           TODO: we should get rid of this hack (cf. BZ#592) *)
         let id = if Id.equal id dummy_name then Id.of_string "__" else id in
-        apply (pr_id id)
+        apply (Id.print id)
     | MLapp (f,args') ->
 	let stl = List.map (pp_expr true env []) args' in
         pp_expr par env (stl @ args) f
@@ -158,7 +159,7 @@ let rec pp_expr par env args =
 	apply2 st
     | MLletin (id,a1,a2) ->
 	let i,env' = push_vars [id_of_mlid id] env in
-	let pp_id = pr_id (List.hd i)
+	let pp_id = Id.print (List.hd i)
 	and pp_a1 = pp_expr false env [] a1
 	and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
 	let pp_def =
@@ -185,7 +186,7 @@ let rec pp_expr par env 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.";
+	  user_err Pp.(str "Cannot mix yet user-given match and general patterns.");
 	let mkfun (ids,_,e) =
 	  if not (List.is_empty ids) then named_lams (List.rev ids) e
 	  else dummy_lams (ast_lift 1 e) 1
@@ -222,10 +223,10 @@ and pp_cons_pat par r ppl =
 
 and pp_gen_pat par ids env = function
   | Pcons (r,l) -> pp_cons_pat par r (List.map (pp_gen_pat true ids env) l)
-  | Pusual r -> pp_cons_pat par r (List.map pr_id ids)
+  | Pusual r -> pp_cons_pat par r (List.map Id.print ids)
   | Ptuple l -> pp_boxed_tuple (pp_gen_pat false ids env) l
   | Pwild -> str "_"
-  | Prel n -> pr_id (get_db_name n env)
+  | Prel n -> Id.print (get_db_name n env)
 
 and pp_one_pat env (ids,p,t) =
   let ids',env' = push_vars (List.rev_map id_of_mlid ids) env in
@@ -250,10 +251,10 @@ and pp_fix par env i (ids,bl) args =
     (v 0
        (v 1 (str "let {" ++ fnl () ++
 	     prvect_with_sep (fun () -> str ";" ++ fnl ())
-	       (fun (fi,ti) -> pp_function env (pr_id fi) ti)
+	       (fun (fi,ti) -> pp_function env (Id.print fi) ti)
 	       (Array.map2 (fun a b -> a,b) ids bl) ++
 	     str "}") ++
-        fnl () ++ str "in " ++ pp_apply (pr_id ids.(i)) false args))
+        fnl () ++ str "in " ++ pp_apply (Id.print ids.(i)) false args))
 
 and pp_function env f t =
   let bl,t' = collect_lams t in
@@ -265,19 +266,19 @@ and pp_function env f t =
 (*s Pretty-printing of inductive types declaration. *)
 
 let pp_logical_ind packet =
-  pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++
+  pp_comment (Id.print packet.ip_typename ++ str " : logical inductive") ++
   pp_comment (str "with constructors : " ++
-	      prvect_with_sep spc pr_id packet.ip_consnames)
+	      prvect_with_sep spc Id.print packet.ip_consnames)
 
 let pp_singleton kn packet =
   let name = pp_global Type (IndRef (kn,0)) in
   let l = rename_tvars keywords packet.ip_vars in
   hov 2 (str "type " ++ name ++ spc () ++
-	 prlist_with_sep spc pr_id l ++
+	 prlist_with_sep spc Id.print l ++
 	 (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)))
+		     Id.print packet.ip_consnames.(0)))
 
 let pp_one_ind ip pl cv =
   let pl = rename_tvars keywords pl in
@@ -329,7 +330,7 @@ let pp_decl = function
 	    let ids,s = find_type_custom r in
 	    prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s
 	  with Not_found ->
-	    prlist (fun id -> pr_id id ++ str " ") l ++
+	    prlist (fun id -> Id.print id ++ str " ") l ++
 	    if t == Taxiom then str "= () -- AXIOM TO BE REALIZED" ++ fnl ()
 	    else str "=" ++ spc () ++ pp_type false l t
 	in
diff --git a/plugins/extraction/haskell.mli b/plugins/extraction/haskell.mli
index 6f493206..27cb6b94 100644
--- a/plugins/extraction/haskell.mli
+++ b/plugins/extraction/haskell.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 val haskell_descr : Miniml.language_descr
diff --git a/plugins/extraction/miniml.ml b/plugins/extraction/miniml.ml
new file mode 100644
index 00000000..e1e49d92
--- /dev/null
+++ b/plugins/extraction/miniml.ml
@@ -0,0 +1,222 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+(*s Target language for extraction: a core ML called MiniML. *)
+
+open Names
+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
+   object. *)
+
+(* We eliminate from terms:
+   1) types
+   2) logical parts
+   3) user-declared implicit arguments of a constant of constructor
+*)
+
+type kill_reason =
+  | Ktype
+  | Kprop
+  | Kimplicit of global_reference * int  (* n-th arg of a cst or construct *)
+
+type sign = Keep | Kill of kill_reason
+
+
+(* Convention: outmost lambda/product gives the head of the list. *)
+
+type signature = sign list
+
+(*s ML type expressions. *)
+
+type ml_type =
+  | Tarr    of ml_type * ml_type
+  | Tglob   of global_reference * ml_type list
+  | Tvar    of int
+  | Tvar'   of int (* same as Tvar, used to avoid clash *)
+  | Tmeta   of ml_meta (* used during ML type reconstruction *)
+  | Tdummy  of kill_reason
+  | Tunknown
+  | Taxiom
+
+and ml_meta = { id : int; mutable contents : ml_type option }
+
+(* ML type schema.
+   The integer is the number of variable in the schema. *)
+
+type ml_schema = int * ml_type
+
+(*s ML inductive types. *)
+
+type inductive_kind =
+  | Singleton
+  | Coinductive
+  | Standard
+  | Record of global_reference option list (* None for anonymous field *)
+
+(* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body].
+   If the inductive is logical ([ip_logical = false]), then all other fields
+   are unused. Otherwise,
+   [ip_sign] is a signature concerning the arguments of the inductive,
+   [ip_vars] contains the names of the type variables surviving in ML,
+   [ip_types] contains the ML types of all constructors.
+*)
+
+type ml_ind_packet = {
+  ip_typename : Id.t;
+  ip_consnames : Id.t array;
+  ip_logical : bool;
+  ip_sign : signature;
+  ip_vars : Id.t list;
+  ip_types : (ml_type list) array
+}
+
+(* [ip_nparams] contains the number of parameters. *)
+
+type equiv =
+  | NoEquiv
+  | Equiv of KerName.t
+  | RenEquiv of string
+
+type ml_ind = {
+  ind_kind : inductive_kind;
+  ind_nparams : int;
+  ind_packets : ml_ind_packet array;
+  ind_equiv : equiv
+}
+
+(*s ML terms. *)
+
+type ml_ident =
+  | Dummy
+  | 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
+    either the type of the applied constructor or the type
+    of the head of the match.
+*)
+
+(** Nota : the constructor [MLtuple] and the extension of [MLcase]
+    to general patterns have been proposed by P.N. Tollitte for
+    his Relation Extraction plugin. [MLtuple] is currently not
+    used by the main extraction, as well as deep patterns. *)
+
+type ml_branch = ml_ident list * ml_pattern * ml_ast
+
+and ml_ast =
+  | MLrel    of int
+  | MLapp    of ml_ast * ml_ast list
+  | MLlam    of ml_ident * ml_ast
+  | MLletin  of ml_ident * ml_ast * ml_ast
+  | MLglob   of global_reference
+  | 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 * Id.t array * ml_ast array
+  | MLexn    of string
+  | MLdummy  of kill_reason
+  | MLaxiom
+  | MLmagic  of ml_ast
+
+and ml_pattern =
+  | Pcons   of global_reference * ml_pattern list
+  | Ptuple  of ml_pattern list
+  | Prel    of int (** Cf. the idents in the branch. [Prel 1] is the last one. *)
+  | Pwild
+  | Pusual  of global_reference (** Shortcut for Pcons (r,[Prel n;...;Prel 1]) **)
+
+(*s ML declarations. *)
+
+type ml_decl =
+  | Dind  of MutInd.t * ml_ind
+  | 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 MutInd.t * ml_ind
+  | Stype of global_reference * Id.t list * ml_type option
+  | Sval  of global_reference * ml_type
+
+type ml_specif =
+  | Spec of ml_spec
+  | Smodule of ml_module_type
+  | Smodtype of ml_module_type
+
+and ml_module_type =
+  | MTident of ModPath.t
+  | MTfunsig of MBId.t * ml_module_type * ml_module_type
+  | MTsig of ModPath.t * ml_module_sig
+  | MTwith of ml_module_type * ml_with_declaration
+
+and ml_with_declaration =
+  | ML_With_type of Id.t list * Id.t list * ml_type
+  | ML_With_module of Id.t list * ModPath.t
+
+and ml_module_sig = (Label.t * ml_specif) list
+
+type ml_structure_elem =
+  | SEdecl of ml_decl
+  | SEmodule of ml_module
+  | SEmodtype of ml_module_type
+
+and ml_module_expr =
+  | MEident of ModPath.t
+  | MEfunctor of MBId.t * ml_module_type * ml_module_expr
+  | MEstruct of ModPath.t * ml_module_structure
+  | MEapply of ml_module_expr * ml_module_expr
+
+and ml_module_structure = (Label.t * ml_structure_elem) list
+
+and ml_module =
+    { ml_mod_expr : ml_module_expr;
+      ml_mod_type : ml_module_type }
+
+(* NB: we do not translate the [mod_equiv] field, since [mod_equiv = mp]
+   implies that [mod_expr = MEBident mp]. Same with [msb_equiv]. *)
+
+type ml_structure = (ModPath.t * ml_module_structure) list
+
+type ml_signature = (ModPath.t * ml_module_sig) list
+
+type unsafe_needs = {
+  mldummy : bool;
+  tdummy : bool;
+  tunknown : bool;
+  magic : bool
+}
+
+type language_descr = {
+  keywords : Id.Set.t;
+
+  (* Concerning the source file *)
+  file_suffix : string;
+  file_naming : ModPath.t -> string;
+  (* the second argument is a comment to add to the preamble *)
+  preamble :
+    Id.t -> Pp.t option -> ModPath.t list -> unsafe_needs ->
+    Pp.t;
+  pp_struct : ml_structure -> Pp.t;
+
+  (* Concerning a possible interface file *)
+  sig_suffix : string option;
+  (* the second argument is a comment to add to the preamble *)
+  sig_preamble :
+    Id.t -> Pp.t option -> ModPath.t list -> unsafe_needs ->
+    Pp.t;
+  pp_sig : ml_signature -> Pp.t;
+
+  (* for an isolated declaration print *)
+  pp_decl : ml_decl -> Pp.t;
+
+}
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index db336152..e1e49d92 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -1,14 +1,15 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*s Target language for extraction: a core ML called MiniML. *)
 
-open Pp
 open Names
 open Globnames
 
@@ -82,7 +83,7 @@ type ml_ind_packet = {
 
 type equiv =
   | NoEquiv
-  | Equiv of kernel_name
+  | Equiv of KerName.t
   | RenEquiv of string
 
 type ml_ind = {
@@ -137,13 +138,13 @@ and ml_pattern =
 (*s ML declarations. *)
 
 type ml_decl =
-  | Dind  of mutual_inductive * ml_ind
+  | Dind  of MutInd.t * ml_ind
   | 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
+  | Sind  of MutInd.t * ml_ind
   | Stype of global_reference * Id.t list * ml_type option
   | Sval  of global_reference * ml_type
 
@@ -153,14 +154,14 @@ type ml_specif =
   | Smodtype of ml_module_type
 
 and ml_module_type =
-  | MTident of module_path
+  | MTident of ModPath.t
   | MTfunsig of MBId.t * ml_module_type * ml_module_type
-  | MTsig of module_path * ml_module_sig
+  | MTsig of ModPath.t * ml_module_sig
   | MTwith of ml_module_type * ml_with_declaration
 
 and ml_with_declaration =
   | ML_With_type of Id.t list * Id.t list * ml_type
-  | ML_With_module of Id.t list * module_path
+  | ML_With_module of Id.t list * ModPath.t
 
 and ml_module_sig = (Label.t * ml_specif) list
 
@@ -170,9 +171,9 @@ type ml_structure_elem =
   | SEmodtype of ml_module_type
 
 and ml_module_expr =
-  | MEident of module_path
+  | MEident of ModPath.t
   | MEfunctor of MBId.t * ml_module_type * ml_module_expr
-  | MEstruct of module_path * ml_module_structure
+  | MEstruct of ModPath.t * ml_module_structure
   | MEapply of ml_module_expr * ml_module_expr
 
 and ml_module_structure = (Label.t * ml_structure_elem) list
@@ -184,11 +185,9 @@ and ml_module =
 (* NB: we do not translate the [mod_equiv] field, since [mod_equiv = mp]
    implies that [mod_expr = MEBident mp]. Same with [msb_equiv]. *)
 
-type ml_structure = (module_path * ml_module_structure) list
+type ml_structure = (ModPath.t * ml_module_structure) list
 
-type ml_signature = (module_path * ml_module_sig) list
-
-type ml_flat_structure = ml_structure_elem list
+type ml_signature = (ModPath.t * ml_module_sig) list
 
 type unsafe_needs = {
   mldummy : bool;
@@ -202,22 +201,22 @@ type language_descr = {
 
   (* Concerning the source file *)
   file_suffix : string;
-  file_naming : module_path -> string;
+  file_naming : ModPath.t -> string;
   (* 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;
+    Id.t -> Pp.t option -> ModPath.t list -> unsafe_needs ->
+    Pp.t;
+  pp_struct : ml_structure -> Pp.t;
 
   (* Concerning a possible interface file *)
   sig_suffix : string option;
   (* 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;
+    Id.t -> Pp.t option -> ModPath.t list -> unsafe_needs ->
+    Pp.t;
+  pp_sig : ml_signature -> Pp.t;
 
   (* for an isolated declaration print *)
-  pp_decl : ml_decl -> std_ppcmds;
+  pp_decl : ml_decl -> Pp.t;
 
 }
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 402fe4ff..0656d487 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*i*)
@@ -28,9 +30,9 @@ let dummy_name = Id.of_string "_"
 let anonymous = Id anonymous_name
 
 let id_of_name = function
-  | Anonymous -> anonymous_name
-  | Name id when Id.equal id dummy_name -> anonymous_name
-  | Name id -> id
+  | Name.Anonymous -> anonymous_name
+  | Name.Name id when Id.equal id dummy_name -> anonymous_name
+  | Name.Name id -> id
 
 let id_of_mlid = function
   | Dummy -> dummy_name
@@ -120,7 +122,6 @@ let rec mgu = function
       mgu (a, a'); mgu (b, b')
   | 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 _ -> ()
   | Tvar i, Tvar j when Int.equal i j -> ()
   | Tvar' i, Tvar' j when  Int.equal i j -> ()
@@ -128,11 +129,15 @@ let rec mgu = function
   | Taxiom, Taxiom -> ()
   | _ -> raise Impossible
 
-let needs_magic p = try mgu p; false with Impossible -> true
+let skip_typing () = lang () == Scheme || is_extrcompute ()
 
-let put_magic_if b a = if b && lang () != Scheme then MLmagic a else a
+let needs_magic p =
+  if skip_typing () then false
+  else try mgu p; false with Impossible -> true
 
-let put_magic p a = if needs_magic p && lang () != Scheme then MLmagic a else a
+let put_magic_if b a = if b then MLmagic a else a
+
+let put_magic p a = if needs_magic p then MLmagic a else a
 
 let generalizable a =
   lang () != Ocaml ||
@@ -770,6 +775,20 @@ let eta_red e =
 	else e
     | _ -> e
 
+(* Performs an eta-reduction when the core is atomic,
+   or otherwise returns None *)
+
+let atomic_eta_red e =
+  let ids,t = collect_lams e in
+  let n = List.length ids in
+  match t with
+  | MLapp (f,a) when test_eta_args_lift 0 n a ->
+     (match f with
+      | MLrel k when k>n -> Some (MLrel (k-n))
+      | MLglob _ | MLexn _ | MLdummy _ -> Some f
+      | _ -> None)
+  | _ -> None
+
 (*s Computes all head linear beta-reductions possible in [(t a)].
   Non-linear head beta-redex become let-in. *)
 
@@ -1052,7 +1071,12 @@ let rec simpl o = function
   | MLmagic(MLcase(typ,e,br)) ->
      let br' = Array.map (fun (ids,p,c) -> (ids,p,MLmagic c)) br in
      simpl o (MLcase(typ,e,br'))
+  | MLmagic(MLdummy _ as e) when lang () == Haskell -> e
   | MLmagic(MLexn _ as e) -> e
+  | MLlam _ as e ->
+     (match atomic_eta_red e with
+      | Some e' -> e'
+      | None -> ast_map (simpl o) e)
   | a -> ast_map (simpl o) a
 
 (* invariant : list [a] of arguments is non-empty *)
@@ -1487,7 +1511,7 @@ let inline_test r t =
 
 let con_of_string s =
   let d, id = Libnames.split_dirpath (dirpath_of_string s) in
-  Constant.make2 (MPfile d) (Label.of_id id)
+  Constant.make2 (ModPath.MPfile d) (Label.of_id id)
 
 let manual_inline_set =
   List.fold_right (fun x -> Cset_env.add (con_of_string x))
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index c6675524..55a1ee89 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Names
@@ -48,7 +50,7 @@ end
 
 (*s Utility functions over ML types without meta *)
 
-val type_mem_kn : mutual_inductive -> ml_type -> bool
+val type_mem_kn : MutInd.t -> ml_type -> bool
 
 val type_maxvar : ml_type -> int
 
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 60fe8e76..f33a59ed 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -1,12 +1,15 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Names
+open ModPath
 open Globnames
 open CErrors
 open Util
@@ -16,10 +19,15 @@ open Mlutil
 
 (*S Functions upon ML modules. *)
 
+(** Note: a syntax like [(F M) with ...] is actually legal, see for instance
+    bug #4720. Hence the code below tries to handle [MTsig], maybe not in
+    a perfect way, but that should be enough for the use of [se_iter] below. *)
+
 let rec msid_of_mt = function
   | MTident mp -> mp
+  | MTsig(mp,_) -> mp
   | MTwith(mt,_)-> msid_of_mt mt
-  | _ -> anomaly ~label:"extraction" (Pp.str "the With operator isn't applied to a name")
+  | MTfunsig _ -> assert false (* A functor cannot be inside a MTwith *)
 
 (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a
    [ml_structure]. *)
@@ -35,7 +43,7 @@ let se_iter do_decl do_spec do_mp =
 	  List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl'
 	in
 	let r = ConstRef (Constant.make2 mp_w (Label.of_id l')) in
-	mt_iter mt; do_decl (Dtype(r,l,t))
+        mt_iter mt; do_spec (Stype(r,l,Some t))
     | MTwith (mt,ML_With_module(idl,mp))->
         let mp_mt = msid_of_mt mt in
         let mp_w =
@@ -110,7 +118,7 @@ let ind_iter_references do_term do_cons do_type kn ind =
     do_type (IndRef ip);
     if lang () == Ocaml then
       (match ind.ind_equiv with
-	 | Miniml.Equiv kne -> do_type (IndRef (mind_of_kn kne, snd ip));
+	 | Miniml.Equiv kne -> do_type (IndRef (MutInd.make1 kne, snd ip));
 	 | _ -> ());
     Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types
   in
@@ -231,7 +239,7 @@ let get_decl_in_structure r struc =
 		  | _ -> error_not_visible r
     in go ll sel
   with Not_found ->
-    anomaly (Pp.str "reference not found in extracted structure")
+    anomaly (Pp.str "reference not found in extracted structure.")
 
 
 (*s Optimization of a [ml_structure]. *)
diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli
index dc870824..6a81f270 100644
--- a/plugins/extraction/modutil.mli
+++ b/plugins/extraction/modutil.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Names
@@ -17,6 +19,7 @@ val struct_type_search : (ml_type -> bool) -> ml_structure -> bool
 
 type do_ref = global_reference -> unit
 
+val type_iter_references : do_ref -> ml_type -> 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
@@ -25,7 +28,7 @@ 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 msid_of_mt : ml_module_type -> ModPath.t
 
 val get_decl_in_structure : global_reference -> ml_structure -> ml_decl
 
@@ -36,5 +39,5 @@ val get_decl_in_structure : global_reference -> ml_structure -> ml_decl
    optimizations. The first argument is the list of objects we want to appear.
 *)
 
-val optimize_struct : global_reference list * module_path list ->
+val optimize_struct : global_reference list * ModPath.t list ->
   ml_structure -> ml_structure
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 1c29a9bc..96d87604 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*s Production of Ocaml syntax. *)
@@ -12,7 +14,7 @@ open Pp
 open CErrors
 open Util
 open Names
-open Nameops
+open ModPath
 open Globnames
 open Table
 open Miniml
@@ -28,7 +30,7 @@ let pp_tvar id = str ("'" ^ Id.to_string id)
 let pp_abst = function
   | [] -> mt ()
   | l  ->
-      str "fun " ++ prlist_with_sep (fun () -> str " ") pr_id l ++
+      str "fun " ++ prlist_with_sep (fun () -> str " ") Id.print l ++
       str " ->" ++ spc ()
 
 let pp_parameters l =
@@ -66,7 +68,7 @@ let pp_header_comment = function
   | None -> mt ()
   | Some com -> pp_comment com ++ fnl2 ()
 
-let then_nl pp = if Pp.is_empty pp then mt () else pp ++ fnl ()
+let then_nl pp = if Pp.ismt pp then mt () else pp ++ fnl ()
 
 let pp_tdummy usf =
   if usf.tdummy || usf.tunknown then str "type __ = Obj.t" ++ fnl () else mt ()
@@ -100,11 +102,41 @@ let pp_global k r = str (str_global k r)
 
 let pp_modname mp = str (Common.pp_module mp)
 
+(* grammar from OCaml 4.06 manual, "Prefix and infix symbols" *)
+
+let infix_symbols =
+  ['=' ; '<' ; '>' ; '@' ; '^' ; ';' ; '&' ; '+' ; '-' ; '*' ; '/' ; '$' ; '%' ]
+let operator_chars =
+  [ '!' ; '$' ; '%' ; '&' ; '*' ; '+' ; '-' ; '.' ; '/' ; ':' ; '<' ; '=' ; '>' ; '?' ; '@' ; '^' ; '|' ; '~' ]
+
+(* infix ops in OCaml, but disallowed by preceding grammar *)
+
+let builtin_infixes =
+  [ "::" ; "," ]
+
+let substring_all_opchars s start stop =
+  let rec check_char i =
+    if i >= stop then true
+    else
+      List.mem s.[i] operator_chars && check_char (i+1)
+  in
+  check_char start
+
 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] == ')')
+   let len = String.length s in
+   len >= 3 &&
+   (* parenthesized *)
+   (s.[0] == '(' && s.[len-1] == ')' &&
+      let inparens = String.trim (String.sub s 1 (len - 2)) in
+      let inparens_len = String.length inparens in
+      (* either, begins with infix symbol, any remainder is all operator chars *)
+      (List.mem inparens.[0] infix_symbols && substring_all_opchars inparens 1 inparens_len) ||
+      (* or, starts with #, at least one more char, all are operator chars *)
+      (inparens.[0] == '#' && inparens_len >= 2 && substring_all_opchars inparens 1 inparens_len) ||
+      (* or, is an OCaml built-in infix *)
+      (List.mem inparens builtin_infixes)))
 
 let get_infix r =
   let s = find_custom r in
@@ -182,7 +214,7 @@ let rec pp_expr par env args =
         (* Try to survive to the occurrence of a Dummy rel.
            TODO: we should get rid of this hack (cf. #592) *)
         let id = if Id.equal id dummy_name then Id.of_string "__" else id in
-        apply (pr_id id)
+        apply (Id.print id)
     | MLapp (f,args') ->
 	let stl = List.map (pp_expr true env []) args' in
         pp_expr par env (stl @ args) f
@@ -194,7 +226,7 @@ let rec pp_expr par env args =
 	apply2 st
     | MLletin (id,a1,a2) ->
 	let i,env' = push_vars [id_of_mlid id] env in
-	let pp_id = pr_id (List.hd i)
+	let pp_id = Id.print (List.hd i)
 	and pp_a1 = pp_expr false env [] a1
 	and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
 	hv 0 (apply2 (pp_letin pp_id pp_a1 pp_a2))
@@ -246,7 +278,7 @@ let rec pp_expr par env 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.";
+	  user_err Pp.(str "Cannot mix yet user-given match and general patterns.");
 	let mkfun (ids,_,e) =
 	  if not (List.is_empty ids) then named_lams (List.rev ids) e
 	  else dummy_lams (ast_lift 1 e) 1
@@ -330,10 +362,10 @@ and pp_cons_pat r ppl =
 
 and pp_gen_pat ids env = function
   | Pcons (r, l) -> pp_cons_pat r (List.map (pp_gen_pat ids env) l)
-  | Pusual r -> pp_cons_pat r (List.map pr_id ids)
+  | Pusual r -> pp_cons_pat r (List.map Id.print ids)
   | Ptuple l -> pp_boxed_tuple (pp_gen_pat ids env) l
   | Pwild -> str "_"
-  | Prel n -> pr_id (get_db_name n env)
+  | Prel n -> Id.print (get_db_name n env)
 
 and pp_ifthenelse env expr pv = match pv with
   | [|([],tru,the);([],fal,els)|] when
@@ -372,7 +404,7 @@ and pp_function env t =
 	  v 0 (pp_pat env' pv)
 	else
           pr_binding (List.rev bl) ++
-          str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++
+          str " = match " ++ Id.print (List.hd bl) ++ str " with" ++ fnl () ++
 	  v 0 (pp_pat env' pv)
     | _ ->
           pr_binding (List.rev bl) ++
@@ -387,10 +419,10 @@ and pp_fix par env i (ids,bl) args =
     (v 0 (str "let rec " ++
 	  prvect_with_sep
       	    (fun () -> fnl () ++ str "and ")
-	    (fun (fi,ti) -> pr_id fi ++ pp_function env ti)
+	    (fun (fi,ti) -> Id.print fi ++ pp_function env ti)
 	    (Array.map2 (fun id b -> (id,b)) ids bl) ++
 	  fnl () ++
-	  hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))
+	  hov 2 (str "in " ++ pp_apply (Id.print ids.(i)) false args)))
 
 (* Ad-hoc double-newline in v boxes, with enough negative whitespace
    to avoid indenting the intermediate blank line *)
@@ -431,7 +463,7 @@ let pp_Dfix (rv,c,t) =
 let pp_equiv param_list name = function
   | NoEquiv, _ -> mt ()
   | Equiv kn, i ->
-      str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (mind_of_kn kn,i))
+      str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (MutInd.make1 kn,i))
   | RenEquiv ren, _  ->
       str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name
 
@@ -451,10 +483,10 @@ let pp_one_ind prefix ip_equiv pl name cnames ctyps =
   else fnl () ++ v 0 (prvecti pp_constructor ctyps)
 
 let pp_logical_ind packet =
-  pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++
+  pp_comment (Id.print packet.ip_typename ++ str " : logical inductive") ++
   fnl () ++
   pp_comment (str "with constructors : " ++
-	      prvect_with_sep spc pr_id packet.ip_consnames) ++
+	      prvect_with_sep spc Id.print packet.ip_consnames) ++
   fnl ()
 
 let pp_singleton kn packet =
@@ -463,7 +495,7 @@ let pp_singleton kn packet =
   hov 2 (str "type " ++ pp_parameters l ++ name ++ 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)))
+		     Id.print packet.ip_consnames.(0)))
 
 let pp_record kn fields ip_equiv packet =
   let ind = IndRef (kn,0) in
@@ -555,24 +587,6 @@ let pp_decl = function
     | Dfix (rv,defs,typs) ->
 	pp_Dfix (rv,defs,typs)
 
-let pp_alias_decl ren = function
-  | Dind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
-  | Dtype (r, l, _) ->
-      let name = pp_global Type r in
-      let l = rename_tvars keywords l in
-      let ids = pp_parameters l in
-      hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++
-	     str (ren^".") ++ name)
-  | Dterm (r, a, t) ->
-      let name = pp_global Term r in
-      hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name)
-  | Dfix (rv, _, _) ->
-      prvecti (fun i r -> if is_inline_custom r then mt () else
-		 let name = pp_global Term r in
-		 hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) ++
-		 fnl ())
-	rv
-
 let pp_spec = function
   | Sval (r,_) when is_inline_custom r -> mt ()
   | Stype (r,_,_) when is_inline_custom r -> mt ()
@@ -597,42 +611,32 @@ let pp_spec = function
       in
       hov 2 (str "type " ++ ids ++ name ++ def)
 
-let pp_alias_spec ren = function
-  | Sind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren }
-  | Stype (r,l,_) ->
-      let name = pp_global Type r in
-      let l = rename_tvars keywords l in
-      let ids = pp_parameters l in
-      hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++
-	     str (ren^".") ++ name)
-  | Sval _ -> assert false
-
 let rec pp_specif = function
   | (_,Spec (Sval _ as s)) -> pp_spec s
   | (l,Spec s) ->
-      (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
+     (match Common.get_duplicate (top_visible_mp ()) l with
+      | None -> pp_spec s
+      | Some ren ->
 	 hov 1 (str ("module "^ren^" : sig") ++ fnl () ++ pp_spec s) ++
 	 fnl () ++ str "end" ++ fnl () ++
-	 pp_alias_spec ren s
-       with Not_found -> pp_spec s)
+         str ("include module type of struct include "^ren^" end"))
   | (l,Smodule mt) ->
       let def = pp_module_type [] mt in
-      let def' = pp_module_type [] mt in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1 (str "module " ++ name ++ str " :" ++ fnl () ++ def) ++
-      (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
-	 fnl () ++ hov 1 (str ("module "^ren^" :") ++ fnl () ++ def')
-       with Not_found -> Pp.mt ())
+      (match Common.get_duplicate (top_visible_mp ()) l with
+       | None -> Pp.mt ()
+       | Some ren ->
+         fnl () ++
+         hov 1 (str ("module "^ren^" :") ++ spc () ++
+                str "module type of struct include " ++ name ++ str " end"))
   | (l,Smodtype mt) ->
       let def = pp_module_type [] mt in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++
-      (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
-	 fnl () ++ str ("module type "^ren^" = ") ++ name
-       with Not_found -> Pp.mt ())
+      (match Common.get_duplicate (top_visible_mp ()) l with
+       | None -> Pp.mt ()
+       | Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name)
 
 and pp_module_type params = function
   | MTident kn ->
@@ -646,15 +650,17 @@ and pp_module_type params = function
       push_visible mp params;
       let try_pp_specif l x =
         let px = pp_specif x in
-        if Pp.is_empty px then l else px::l
+        if Pp.ismt px then l else px::l
       in
       (* We cannot use fold_right here due to side effects in pp_specif *)
       let l = List.fold_left try_pp_specif [] sign in
       let l = List.rev l in
       pop_visible ();
       str "sig" ++ fnl () ++
-      v 1 (str " " ++ prlist_with_sep cut2 identity l) ++
-	fnl () ++ str "end"
+      (if List.is_empty l then mt ()
+       else
+         v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl ())
+      ++ str "end"
   | 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
@@ -681,12 +687,11 @@ let is_short = function MEident _ | MEapply _ -> true | _ -> false
 
 let rec pp_structure_elem = function
   | (l,SEdecl d) ->
-       (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
+     (match Common.get_duplicate (top_visible_mp ()) l with
+      | None -> pp_decl d
+      | Some ren ->
 	 hov 1 (str ("module "^ren^" = struct") ++ fnl () ++ pp_decl d) ++
-	 fnl () ++ str "end" ++ fnl () ++
-	 pp_alias_decl ren d
-	with Not_found -> pp_decl d)
+	 fnl () ++ str "end" ++ fnl () ++ str ("include "^ren))
   | (l,SEmodule m) ->
       let typ =
         (* virtual printing of the type, in order to have a correct mli later*)
@@ -699,18 +704,16 @@ let rec pp_structure_elem = function
       hov 1
 	(str "module " ++ name ++ typ ++ str " =" ++
 	 (if is_short m.ml_mod_expr then spc () else fnl ()) ++ def) ++
-      (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
-	 fnl () ++ str ("module "^ren^" = ") ++ name
-       with Not_found -> mt ())
+      (match Common.get_duplicate (top_visible_mp ()) l with
+       | Some ren -> fnl () ++ str ("module "^ren^" = ") ++ name
+       | None -> mt ())
   | (l,SEmodtype m) ->
       let def = pp_module_type [] m in
       let name = pp_modname (MPdot (top_visible_mp (), l)) in
       hov 1 (str "module type " ++ name ++ str " =" ++ fnl () ++ def) ++
-      (try
-	 let ren = Common.check_duplicate (top_visible_mp ()) l in
-         fnl () ++ str ("module type "^ren^" = ") ++ name
-       with Not_found -> mt ())
+      (match Common.get_duplicate (top_visible_mp ()) l with
+       | None -> mt ()
+       | Some ren -> fnl () ++ str ("module type "^ren^" = ") ++ name)
 
 and pp_module_expr params = function
   | MEident mp -> pp_modname mp
@@ -725,15 +728,17 @@ and pp_module_expr params = function
       push_visible mp params;
       let try_pp_structure_elem l x =
         let px = pp_structure_elem x in
-        if Pp.is_empty px then l else px::l
+        if Pp.ismt px then l else px::l
       in
       (* We cannot use fold_right here due to side effects in pp_structure_elem *)
       let l = List.fold_left try_pp_structure_elem [] sel in
       let l = List.rev l in
       pop_visible ();
       str "struct" ++ fnl () ++
-      v 1 (str " " ++ prlist_with_sep cut2 identity l) ++
-      fnl () ++ str "end"
+      (if List.is_empty l then mt ()
+       else
+         v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl ())
+      ++ str "end"
 
 let rec prlist_sep_nonempty sep f = function
   | [] -> mt ()
@@ -741,7 +746,7 @@ let rec prlist_sep_nonempty sep f = function
   | h::t ->
      let e = f h in
      let r = prlist_sep_nonempty sep f t in
-     if Pp.is_empty e then r
+     if Pp.ismt e then r
      else e ++ sep () ++ r
 
 let do_struct f s =
diff --git a/plugins/extraction/ocaml.mli b/plugins/extraction/ocaml.mli
index f579a54b..96d12344 100644
--- a/plugins/extraction/ocaml.mli
+++ b/plugins/extraction/ocaml.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 val ocaml_descr : Miniml.language_descr
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index a6309e61..76a0c740 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 (*s Production of Scheme syntax. *)
@@ -40,11 +42,7 @@ let preamble _ comment _ usf =
   (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ())
 
 let pr_id id =
-  let s = Id.to_string id in
-  for i = 0 to String.length s - 1 do
-    if s.[i] == '\'' then s.[i] <- '~'
-  done;
-  str s
+  str @@ String.map (fun c -> if c == '\'' then '~' else c) (Id.to_string id)
 
 let paren = pp_par true
 
@@ -100,9 +98,9 @@ let rec pp_expr env args =
 		 prlist_with_sep spc (pp_cons_args env) args')
 	in
 	if is_coinductive r then paren (str "delay " ++ st) else st
-    | MLtuple _ -> error "Cannot handle tuples in Scheme yet."
+    | MLtuple _ -> user_err Pp.(str "Cannot handle tuples in Scheme yet.")
     | MLcase (_,_,pv) when not (is_regular_match pv) ->
-	error "Cannot handle general patterns in Scheme yet."
+	user_err Pp.(str "Cannot handle general patterns in Scheme yet.")
     | MLcase (_,t,pv) when is_custom_match pv ->
 	let mkfun (ids,_,e) =
 	  if not (List.is_empty ids) then named_lams (List.rev ids) e
diff --git a/plugins/extraction/scheme.mli b/plugins/extraction/scheme.mli
index 5e1ec0d5..defd8184 100644
--- a/plugins/extraction/scheme.mli
+++ b/plugins/extraction/scheme.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 val scheme_descr : Miniml.language_descr
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index ff66d915..54c6d9d7 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -1,15 +1,17 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Names
+open ModPath
 open Term
 open Declarations
-open Nameops
 open Namegen
 open Libobject
 open Goptions
@@ -20,6 +22,11 @@ open Util
 open Pp
 open Miniml
 
+[@@@ocaml.warning "-3"]       (* String.capitalize_ascii since 4.03.0 GPR#124 *)
+let capitalize = String.capitalize
+[@@@ocaml.warning "+3"]
+
+
 (** Sets and maps for [global_reference] that use the "user" [kernel_name]
     instead of the canonical one *)
 
@@ -30,15 +37,14 @@ module Refset' = Refset_env
 
 let occur_kn_in_ref kn = function
   | IndRef (kn',_)
-  | ConstructRef ((kn',_),_) -> Names.eq_mind kn kn'
-  | ConstRef _ -> false
-  | VarRef _ -> assert false
+  | ConstructRef ((kn',_),_) -> MutInd.equal kn kn'
+  | ConstRef _ | VarRef _ -> false
 
 let repr_of_r = function
-  | ConstRef kn -> repr_con kn
+  | ConstRef kn -> Constant.repr3 kn
   | IndRef (kn,_)
-  | ConstructRef ((kn,_),_) -> repr_mind kn
-  | VarRef _ -> assert false
+  | ConstructRef ((kn,_),_) -> MutInd.repr3 kn
+  | VarRef v -> KerName.repr (Lib.make_kn v)
 
 let modpath_of_r r =
   let mp,_,_ = repr_of_r r in mp
@@ -55,11 +61,11 @@ let is_modfile = function
   | _ -> false
 
 let raw_string_of_modfile = function
-  | MPfile f -> String.capitalize (Id.to_string (List.hd (DirPath.repr f)))
+  | MPfile f -> capitalize (Id.to_string (List.hd (DirPath.repr f)))
   | _ -> assert false
 
 let is_toplevel mp =
-  ModPath.equal mp initial_path || ModPath.equal mp (Lib.current_mp ())
+  ModPath.equal mp ModPath.initial || ModPath.equal mp (Lib.current_mp ())
 
 let at_toplevel mp =
   is_modfile mp || is_toplevel mp
@@ -245,6 +251,11 @@ let modular () = !modular_ref
 let set_library b = library_ref := b
 let library () = !library_ref
 
+let extrcompute = ref false
+
+let set_extrcompute b = extrcompute := b
+let is_extrcompute () = !extrcompute
+
 (*s Printing. *)
 
 (* The following functions work even on objects not in [Global.env ()].
@@ -256,18 +267,18 @@ let safe_basename_of_global r =
   let last_chance r =
     try Nametab.basename_of_global r
     with Not_found ->
-      anomaly (Pp.str "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 -> Label.to_id (con_label kn)
-    | IndRef (kn,0) -> Label.to_id (mind_label kn)
+    | ConstRef kn -> Label.to_id (Constant.label kn)
+    | IndRef (kn,0) -> Label.to_id (MutInd.label kn)
     | IndRef (kn,i) ->
       (try (unsafe_lookup_ind kn).ind_packets.(i).ip_typename
        with Not_found -> last_chance r)
     | ConstructRef ((kn,i),j) ->
       (try (unsafe_lookup_ind kn).ind_packets.(i).ip_consnames.(j-1)
        with Not_found -> last_chance r)
-    | VarRef _ -> assert false
+    | VarRef v -> v
 
 let string_of_global r =
  try string_of_qualid (Nametab.shortest_qualid_of_global Id.Set.empty r)
@@ -281,8 +292,8 @@ let safe_pr_long_global r =
   try Printer.pr_global r
   with Not_found -> match r with
     | ConstRef kn ->
-	let mp,_,l = repr_con kn in
-	str ((string_of_mp mp)^"."^(Label.to_string l))
+	let mp,_,l = Constant.repr3 kn in
+	str ((ModPath.to_string mp)^"."^(Label.to_string l))
     | _ -> assert false
 
 let pr_long_mp mp =
@@ -293,7 +304,7 @@ let pr_long_global ref = pr_path (Nametab.path_of_global ref)
 
 (*S Warning and Error messages. *)
 
-let err s = errorlabstrm "Extraction" s
+let err s = user_err ~hdr:"Extraction" s
 
 let warn_extraction_axiom_to_realize =
   CWarnings.create ~name:"extraction-axiom-to-realize" ~category:"extraction"
@@ -411,7 +422,7 @@ let error_singleton_become_prop id og =
                 str " (or in its mutual block)"
     | None -> mt ()
   in
-  err (str "The informative inductive type " ++ pr_id id ++
+  err (str "The informative inductive type " ++ Id.print id ++
        str " has a Prop instance" ++ loc ++ str "." ++ fnl () ++
        str "This happens when a sort-polymorphic singleton inductive type\n" ++
        str "has logical parameters, such as (I,I) : (True * True) : Prop.\n" ++
@@ -439,9 +450,10 @@ let error_MPfile_as_mod mp b =
 	    "Please "^s2^"use (Recursive) Extraction Library instead.\n"))
 
 let argnames_of_global r =
-  let typ = Global.type_of_global_unsafe r in
+  let env = Global.env () in
+  let typ, _ = Global.type_of_global_in_context env r in
   let rels,_ =
-    decompose_prod (Reduction.whd_all (Global.env ()) typ) in
+    decompose_prod (Reduction.whd_all env typ) in
   List.rev_map fst rels
 
 let msg_of_implicit = function
@@ -475,7 +487,7 @@ let check_loaded_modfile mp = match base_mp mp with
       if not (Library.library_is_loaded dp) then begin
 	match base_mp (Lib.current_mp ()) with
 	  | MPfile dp' when not (DirPath.equal dp dp') ->
-	      err (str "Please load library " ++ pr_dirpath dp ++ str " first.")
+            err (str "Please load library " ++ DirPath.print dp ++ str " first.")
 	  | _ -> ()
       end
   | _ -> ()
@@ -494,8 +506,7 @@ let my_bool_option name initval =
   let flag = ref initval in
   let access = fun () -> !flag in
   let _ = declare_bool_option
-    {optsync = true;
-     optdepr = false;
+    {optdepr = false;
      optname = "Extraction "^name;
      optkey = ["Extraction"; name];
      optread = access;
@@ -567,16 +578,14 @@ let chg_flag n = int_flag_ref := n; opt_flag_ref := flag_of_int n
 let optims () = !opt_flag_ref
 
 let _ = declare_bool_option
-	  {optsync = true;
-           optdepr = false;
+	  {optdepr = false;
 	   optname = "Extraction Optimize";
 	   optkey = ["Extraction"; "Optimize"];
 	   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
-          { optsync = true;
-            optdepr = false;
+          { optdepr = false;
             optname = "Extraction Flag";
             optkey = ["Extraction";"Flag"];
             optread = (fun _ -> Some !int_flag_ref);
@@ -590,8 +599,7 @@ let conservative_types_ref = ref false
 let conservative_types () = !conservative_types_ref
 
 let _ = declare_bool_option
-  {optsync = true;
-   optdepr = false;
+  {optdepr = false;
    optname = "Extraction Conservative Types";
    optkey = ["Extraction"; "Conservative"; "Types"];
    optread = (fun () -> !conservative_types_ref);
@@ -603,8 +611,7 @@ let file_comment_ref = ref ""
 let file_comment () = !file_comment_ref
 
 let _ = declare_string_option
-  {optsync = true;
-   optdepr = false;
+  {optdepr = false;
    optname = "Extraction File Comment";
    optkey = ["Extraction"; "File"; "Comment"];
    optread = (fun () -> !file_comment_ref);
@@ -721,7 +728,7 @@ let add_implicits r l =
          let i = List.index Name.equal (Name id) names in
          Int.Set.add i s
        with Not_found ->
-	 err (str "No argument " ++ pr_id id ++ str " for " ++
+	 err (str "No argument " ++ Id.print id ++ str " for " ++
 	      safe_pr_global r)
   in
   let ints = List.fold_left add_arg Int.Set.empty l in
@@ -749,11 +756,11 @@ let extraction_implicit r l =
 
 let blacklist_table = Summary.ref Id.Set.empty ~name:"ExtrBlacklist"
 
-let modfile_ids = ref []
+let modfile_ids = ref Id.Set.empty
 let modfile_mps = ref MPmap.empty
 
 let reset_modfile () =
-  modfile_ids := Id.Set.elements !blacklist_table;
+  modfile_ids := !blacklist_table;
   modfile_mps := MPmap.empty
 
 let string_of_modfile mp =
@@ -762,7 +769,7 @@ let string_of_modfile mp =
     let id = Id.of_string (raw_string_of_modfile mp) in
     let id' = next_ident_away id !modfile_ids in
     let s' = Id.to_string id' in
-    modfile_ids := id' :: !modfile_ids;
+    modfile_ids := Id.Set.add id' !modfile_ids;
     modfile_mps := MPmap.add mp s' !modfile_mps;
     s'
 
@@ -773,13 +780,11 @@ let file_of_modfile mp =
     | 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];
-  s
+  String.mapi (fun i c -> if i = 0 then s0.[0] else c) (string_of_modfile mp)
 
 let add_blacklist_entries l =
   blacklist_table :=
-    List.fold_right (fun s -> Id.Set.add (Id.of_string (String.capitalize s)))
+    List.fold_right (fun s -> Id.Set.add (Id.of_string (capitalize s)))
       l !blacklist_table
 
 (* Registration of operations for rollback. *)
@@ -801,7 +806,7 @@ let extraction_blacklist l =
 (* Printing part *)
 
 let print_extraction_blacklist () =
-  prlist_with_sep fnl pr_id (Id.Set.elements !blacklist_table)
+  prlist_with_sep fnl Id.print (Id.Set.elements !blacklist_table)
 
 (* Reset part *)
 
@@ -879,7 +884,7 @@ let extract_constant_inline inline r ids s =
   match g with
     | ConstRef kn ->
 	let env = Global.env () in
-	let typ = Global.type_of_global_unsafe (ConstRef kn) in
+	let typ, _ = Global.type_of_global_in_context env (ConstRef kn) in
 	let typ = Reduction.whd_all env typ in
 	if Reduction.is_arity env typ
 	  then begin
@@ -894,7 +899,7 @@ let extract_constant_inline inline r ids s =
 let extract_inductive r s l optstr =
   check_inside_section ();
   let g = Smartlocate.global_with_alias r in
-  Dumpglob.add_glob (loc_of_reference r) g;
+  Dumpglob.add_glob ?loc:r.CAst.loc g;
   match g with
     | IndRef ((kn,i) as ip) ->
 	let mib = Global.lookup_mind kn in
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 15a08756..906dfd96 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -1,9 +1,11 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Names
@@ -21,22 +23,22 @@ val safe_basename_of_global : global_reference -> Id.t
 
 val warning_axioms : unit -> unit
 val warning_opaques : bool -> unit
-val warning_ambiguous_name : ?loc:Loc.t -> qualid * module_path * global_reference -> unit
+val warning_ambiguous_name : ?loc:Loc.t -> qualid * ModPath.t * global_reference -> unit
 val warning_id : string -> unit
 val error_axiom_scheme : global_reference -> int -> 'a
 val error_constant : global_reference -> 'a
 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_module_clash : ModPath.t -> ModPath.t -> 'a
+val error_no_module_expr : ModPath.t -> 'a
 val error_singleton_become_prop : Id.t -> global_reference option -> 'a
 val error_unknown_module : qualid -> 'a
 val error_scheme : unit -> 'a
 val error_not_visible : global_reference -> 'a
-val error_MPfile_as_mod : module_path -> bool -> 'a
+val error_MPfile_as_mod : ModPath.t -> bool -> 'a
 val check_inside_module : unit -> unit
 val check_inside_section : unit -> unit
-val check_loaded_modfile : module_path -> unit
+val check_loaded_modfile : ModPath.t -> unit
 val msg_of_implicit : kill_reason -> string
 val err_or_warn_remaining_implicit : kill_reason -> unit
 
@@ -44,22 +46,22 @@ 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 * DirPath.t * Label.t
-val modpath_of_r : global_reference -> module_path
+val occur_kn_in_ref : MutInd.t -> global_reference -> bool
+val repr_of_r : global_reference -> ModPath.t * DirPath.t * Label.t
+val modpath_of_r : global_reference -> ModPath.t
 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
-val file_of_modfile : module_path -> string
-val is_toplevel : module_path -> bool
-val at_toplevel : module_path -> bool
-val mp_length : module_path -> int
-val prefixes_mp : module_path -> MPset.t
+val base_mp : ModPath.t -> ModPath.t
+val is_modfile : ModPath.t -> bool
+val string_of_modfile : ModPath.t -> string
+val file_of_modfile : ModPath.t -> string
+val is_toplevel : ModPath.t -> bool
+val at_toplevel : ModPath.t -> bool
+val mp_length : ModPath.t -> int
+val prefixes_mp : ModPath.t -> MPset.t
 val common_prefix_from_list :
-  module_path -> module_path list -> module_path option
-val get_nth_label_mp : int -> module_path -> Label.t
-val labels_of_ref : global_reference -> module_path * Label.t list
+  ModPath.t -> ModPath.t list -> ModPath.t option
+val get_nth_label_mp : int -> ModPath.t -> Label.t
+val labels_of_ref : global_reference -> ModPath.t * Label.t list
 
 (*s Some table-related operations *)
 
@@ -71,16 +73,16 @@ val labels_of_ref : global_reference -> module_path * Label.t list
    [mutual_inductive_body] as checksum. In both case, we should ideally
    also check the env *)
 
-val add_typedef : constant -> constant_body -> ml_type -> unit
-val lookup_typedef : constant -> constant_body -> ml_type option
+val add_typedef : Constant.t -> constant_body -> ml_type -> unit
+val lookup_typedef : Constant.t -> constant_body -> ml_type option
 
-val add_cst_type : constant -> constant_body -> ml_schema -> unit
-val lookup_cst_type : constant -> constant_body -> ml_schema option
+val add_cst_type : Constant.t -> constant_body -> ml_schema -> unit
+val lookup_cst_type : Constant.t -> constant_body -> ml_schema option
 
-val add_ind : mutual_inductive -> mutual_inductive_body -> ml_ind -> unit
-val lookup_ind : mutual_inductive -> mutual_inductive_body -> ml_ind option
+val add_ind : MutInd.t -> mutual_inductive_body -> ml_ind -> unit
+val lookup_ind : MutInd.t -> mutual_inductive_body -> ml_ind option
 
-val add_inductive_kind : mutual_inductive -> inductive_kind -> unit
+val add_inductive_kind : MutInd.t -> inductive_kind -> unit
 val is_coinductive : global_reference -> bool
 val is_coinductive_type : ml_type -> bool
 (* What are the fields of a record (empty for a non-record) *)
@@ -88,10 +90,10 @@ val get_record_fields :
   global_reference -> global_reference option list
 val record_fields_of_type : ml_type -> global_reference option list
 
-val add_recursors : Environ.env -> mutual_inductive -> unit
+val add_recursors : Environ.env -> MutInd.t -> unit
 val is_recursor : global_reference -> bool
 
-val add_projection : int -> constant -> inductive -> unit
+val add_projection : int -> Constant.t -> inductive -> unit
 val is_projection : global_reference -> bool
 val projection_arity : global_reference -> int
 val projection_info : global_reference -> inductive * int (* arity *)
@@ -165,6 +167,9 @@ val modular : unit -> bool
 val set_library : bool -> unit
 val library : unit -> bool
 
+val set_extrcompute : bool -> unit
+val is_extrcompute : unit -> bool
+
 (*s Table for custom inlining *)
 
 val to_inline : global_reference -> bool
@@ -177,7 +182,7 @@ val implicits_of_global : global_reference -> Int.Set.t
 (*s Table for user-given custom ML extractions. *)
 
 (* UGLY HACK: registration of a function defined in [extraction.ml] *)
-val type_scheme_nb_args_hook : (Environ.env -> Term.constr -> int) Hook.t
+val type_scheme_nb_args_hook : (Environ.env -> Constr.t -> int) Hook.t
 
 val is_custom : global_reference -> bool
 val is_inline_custom : global_reference -> bool
@@ -191,7 +196,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 -> Pp.std_ppcmds
+val print_extraction_inline : unit -> Pp.t
 val reset_extraction_inline : unit -> unit
 val extract_constant_inline :
   bool -> reference -> string list -> string -> unit
@@ -206,7 +211,7 @@ val extraction_implicit : reference -> int_or_id list -> unit
 
 val extraction_blacklist : Id.t list -> unit
 val reset_extraction_blacklist : unit -> unit
-val print_extraction_blacklist : unit -> Pp.std_ppcmds
+val print_extraction_blacklist : unit -> Pp.t
 
 
 
diff --git a/plugins/extraction/vo.itarget b/plugins/extraction/vo.itarget
deleted file mode 100644
index 9c30c5eb..00000000
--- a/plugins/extraction/vo.itarget
+++ /dev/null
@@ -1,16 +0,0 @@
-ExtrHaskellBasic.vo
-ExtrHaskellNatNum.vo
-ExtrHaskellNatInt.vo
-ExtrHaskellNatInteger.vo
-ExtrHaskellZNum.vo
-ExtrHaskellZInt.vo
-ExtrHaskellZInteger.vo
-ExtrHaskellString.vo
-ExtrOcamlBasic.vo
-ExtrOcamlIntConv.vo
-ExtrOcamlBigIntConv.vo
-ExtrOcamlNatInt.vo
-ExtrOcamlNatBigInt.vo
-ExtrOcamlZInt.vo
-ExtrOcamlZBigInt.vo
-ExtrOcamlString.vo