3 files changed, 13 insertions, 12 deletions
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 7014df83fd..657a91c0c1 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -177,8 +177,7 @@ let factor_fix env l cb msb =
 
 let expand_mexpr env mp me =
   let inl = Some (Flags.get_inline_level()) in
-  let sign,_,_,_ = Mod_typing.translate_mse env (Some mp) inl me in
-  sign
+  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. *)
@@ -231,10 +230,9 @@ let rec extract_structure_spec env mp reso = function
 
 (* From [module_expression] to specifications *)
 
-(* Invariant: the [me] given to [extract_mexpr_spec] should either come
-   from a [mod_type] or [type_expr] field, or their [_alg] counterparts.
-   This way, any encountered [MEident] should be a true module type.
-*)
+(* Invariant: the [me_alg] given to [extract_mexpr_spec] and
+   [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
   | MEident mp -> Visit.add_mp_all mp; MTident mp
@@ -247,7 +245,9 @@ and extract_mexpr_spec env mp1 (me_struct,me_alg) = match me_alg with
   | MEwith(me',WithMod(idl,mp))->
       Visit.add_mp_all mp;
       MTwith(extract_mexpr_spec env mp1 (me_struct,me'), ML_With_module(idl,mp))
-  | MEapply _ -> extract_msignature_spec env mp1 no_delta (*TODO*) me_struct
+  | MEapply _ ->
+     (* No higher-order module type in OCaml : we use the expanded version *)
+     extract_msignature_spec env mp1 no_delta (*TODO*) me_struct
 
 and extract_mexpression_spec env mp1 (me_struct,me_alg) = match me_alg with
   | MoreFunctor (mbid, mtb, me_alg') ->
@@ -335,7 +335,8 @@ and extract_mexpr env mp = function
       (* In Haskell/Scheme, we expand everything.
          For now, we also extract everything, dead code will be removed later
          (see [Modutil.optimize_struct]. *)
-      extract_msignature env mp no_delta ~all:true (expand_mexpr env mp me)
+      let sign,_,delta,_ = expand_mexpr env 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;
       Visit.add_mp_all mp; Miniml.MEident mp
@@ -541,7 +542,7 @@ let print_structure_to_file (fn,si,mo) dry struc =
     (if dry then None else si);
   (* Print the buffer content via Coq standard formatter (ok with coqide). *)
   if not (Int.equal (Buffer.length buf) 0) then begin
-    Pp.msg_info (str (Buffer.contents buf));
+    Pp.msg_notice (str (Buffer.contents buf));
     Buffer.reset buf
   end
 
@@ -635,7 +636,7 @@ let simple_extraction r =
       in
       let ans = flag ++ print_one_decl struc (modpath_of_r r) d in
       reset ();
-      Pp.msg_info ans
+      Pp.msg_notice ans
   | _ -> assert false
 
 
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index 9feaea8cdb..30486879ee 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -453,7 +453,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 "^(DirPath.to_string dp^" first.")))
+	      err (str "Please load library " ++ pr_dirpath dp ++ str " first.")
 	  | _ -> ()
       end
   | _ -> ()
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 916cf3ad6b..4e638a0ace 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -13,7 +13,7 @@ open Miniml
 open Declarations
 
 module Refset' : CSig.SetS with type elt = global_reference
-module Refmap' : Map.S with type key = global_reference
+module Refmap' : CSig.MapS with type key = global_reference
 
 val safe_basename_of_global : global_reference -> Id.t