Beaoucoup de changements dans la representation interne des modules.

kernel:

-declaration.ml
   unification des representations pour les modules et modules types.
     (type struct_expr_body)

-mod_typing.ml
   le typage des modules est separe de l'evaluation des modules

-modops.ml
   nouvelle fonction qui pour toutes expressions de structure calcule
   sa forme evaluee.(eval_struct)

-safe_typing.ml
  ajout du support du nouvel operateur Include.(add_include).


library:

-declaremods.ml
   nouveaux objets Include et Module-alias et gestion de la resolution de noms pour
   les alias via la nametab.

parsing:

-g_vernac.ml4:
   nouvelles regles pour le support des Includes et pour l'application des signatures
   fonctorielles.


extraction:
  Adaptation a la nouvelle representation des modules et support de l'operateur with.




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

8 files changed, 203 insertions, 83 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 855990d25..7a6d42428 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -289,6 +289,7 @@ let modfstlev_rename l =
     else
       (add_modfstlev id []; s)
 
+
 (*s Creating renaming for a [module_path] *)
 
 let rec mp_create_renaming mp = 
@@ -358,14 +359,14 @@ let create_modular_renamings struc =
   (* 3) determines the potential clashes *)
   let needs_qualify k r = 
     let mp = modpath_of_r r in 
-    if (is_modfile mp) && mp <> current_module && 
-      (clash (ext_mpmem k) mp (List.hd (get_renaming r)) opened_modules)
-    then add_static_clash r
+      if (is_modfile mp) && mp <> current_module && 
+	(clash (ext_mpmem k) mp (List.hd (get_renaming r)) opened_modules)
+      then add_static_clash r
   in
-  Refset.iter (needs_qualify Type) ty;
-  Refset.iter (needs_qualify Term) tr;
-  Refset.iter (needs_qualify Cons) co;
-  List.rev opened_modules
+    Refset.iter (needs_qualify Type) ty;
+    Refset.iter (needs_qualify Term) tr;
+    Refset.iter (needs_qualify Cons) co;
+    List.rev opened_modules
 
 (*s Initial renamings creation, for monolithic extraction. *)
 
@@ -479,3 +480,16 @@ let pp_module mp =
 	    error_module_clash base_s
 	  else dottify ls
 
+
+(*i 
+  (* DO NOT REMOVE: used when making names resolution *)
+  let cout = open_out (f^".ren") in 
+  let ft = Pp_control.with_output_to cout in
+  Hashtbl.iter 
+    (fun r id -> 
+       if short_module r = !current_module then 
+	 msgnl_with ft (pr_id id ++ str " " ++ pr_sp (sp_of_r r)))
+    renamings;
+  pp_flush_with ft ();
+  close_out cout;
+i*)    
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 2aca56f9b..701b71a4a 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -31,16 +31,17 @@ let toplevel_env () =
     | (_,kn), Lib.Leaf o ->
 	let mp,_,l = repr_kn kn in 
 	let seb = match Libobject.object_tag o with
-	  | "CONSTANT" -> SEBconst (Global.lookup_constant (constant_of_kn kn))
-	  | "INDUCTIVE" -> SEBmind (Global.lookup_mind kn) 
-	  | "MODULE" -> SEBmodule (Global.lookup_module (MPdot (mp,l)))
-	  | "MODULE TYPE" -> SEBmodtype (Global.lookup_modtype kn)
+	  | "CONSTANT" -> SFBconst (Global.lookup_constant (constant_of_kn kn))
+	  | "INDUCTIVE" -> SFBmind (Global.lookup_mind kn) 
+	  | "MODULE" -> SFBmodule (Global.lookup_module (MPdot (mp,l)))
+	  | "MODULE TYPE" -> 
+	      SFBmodtype (fst (Global.lookup_modtype (MPdot (mp,l))))
 	  | _ -> failwith "caught"
 	in l,seb
     | _ -> failwith "caught"
   in 
   match current_toplevel () with 
-    | MPself msid -> MEBstruct (msid, List.rev (map_succeed get_reference seg))
+    | MPself msid -> SEBstruct (msid, List.rev (map_succeed get_reference seg))
     | _ -> assert false
 
 let environment_until dir_opt = 
@@ -132,7 +133,7 @@ let factor_fix env l cb msb =
     list_iter_i 
       (fun j -> 
 	 function 
-	   | (l,SEBconst cb') -> 
+	   | (l,SFBconst cb') -> 
 	       if check <> check_fix env cb' (j+1) then raise Impossible; 
 	       labels.(j+1) <- l; 
 	   | _ -> raise Impossible) msb'; 
@@ -141,7 +142,7 @@ let factor_fix env l cb msb =
 
 let rec extract_msig env mp = function 
   | [] -> [] 
-  | (l,SPBconst cb) :: msig -> 
+  | (l,SFBconst cb) :: msig -> 
       let kn = make_con mp empty_dirpath l in 
       let s = extract_constant_spec env kn cb in 
       if logical_spec s then extract_msig env mp msig
@@ -149,7 +150,7 @@ let rec extract_msig env mp = function
 	Visit.add_spec_deps s;
 	(l,Spec s) :: (extract_msig env mp msig)
       end
-  | (l,SPBmind cb) :: msig -> 
+  | (l,SFBmind cb) :: msig -> 
       let kn = make_kn mp empty_dirpath l in 
       let s = Sind (kn, extract_inductive env kn) in 
       if logical_spec s then extract_msig env mp msig
@@ -157,26 +158,42 @@ let rec extract_msig env mp = function
 	Visit.add_spec_deps s;
 	(l,Spec s) :: (extract_msig env mp msig)
       end
-  | (l,SPBmodule {msb_modtype=mtb}) :: msig -> 
-      (l,Smodule (extract_mtb env mtb)) :: (extract_msig env mp msig)
-  | (l,SPBmodtype mtb) :: msig -> 
+  | (l,SFBmodule mb) :: msig -> 
+      (l,Smodule (extract_mtb env (Modops.type_of_mb env mb))) :: 
+	(extract_msig env mp msig)
+  | (l,SFBmodtype mtb) :: msig -> 
       (l,Smodtype (extract_mtb env mtb)) :: (extract_msig env mp msig)
 
-and extract_mtb env = function 
-  | MTBident kn -> Visit.add_kn kn; MTident kn 
-  | MTBfunsig (mbid, mtb, mtb') -> 
+
+and extract_mtb env = function
+  | SEBident kn -> Visit.add_mp kn; MTident kn 
+  | SEBwith(mtb',With_definition_body(idl,cb))->
+      begin
+	let mtb''= extract_mtb env mtb' in
+	    match extract_with_type env cb with (* cb peut contenir des kn  *)
+		None ->  mtb''
+	      | Some (vl,typ) -> MTwith(mtb'',ML_With_type(idl,vl,typ))
+      end
+  | SEBwith(mtb',With_module_body(idl,mp,_))-> 
+      Visit.add_mp mp;
+      MTwith(extract_mtb env mtb',ML_With_module(idl,mp))
+  | SEBfunctor (mbid, mtb, mtb') -> 
       let mp = MPbound mbid in 
       let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in 
-      MTfunsig (mbid, extract_mtb env mtb, 
-		extract_mtb env' mtb') 
-  | MTBsig (msid, msig) -> 
+	MTfunsig (mbid, extract_mtb env mtb, 
+		  extract_mtb env' mtb') 
+  | SEBstruct (msid, msig) -> 
       let mp = MPself msid in 
       let env' = Modops.add_signature mp msig env in 
-      MTsig (msid, extract_msig env' mp msig) 
+	MTsig (msid, extract_msig env' mp msig) 
+  | mtb  -> 
+      let mtb' = Modops.eval_struct env mtb in 
+	extract_mtb env mtb'
+
 
 let rec extract_msb env mp all = function 
   | [] -> [] 
-  | (l,SEBconst cb) :: msb -> 
+  | (l,SFBconst cb) :: msb -> 
       (try 
 	 let vl,recd,msb = factor_fix env l cb msb in 
 	 let vc = Array.map (make_con mp empty_dirpath) vl in
@@ -196,7 +213,7 @@ let rec extract_msb env mp all = function
 	   if (not b) && (logical_decl d) then ms 
 	   else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
 	 else ms)
-  | (l,SEBmind mib) :: msb ->
+  | (l,SFBmind mib) :: msb ->
       let ms = extract_msb env mp all msb in
       let kn = make_kn mp empty_dirpath l in 
       let b = Visit.needed_kn kn in
@@ -205,50 +222,52 @@ let rec extract_msb env mp all = function
 	if (not b) && (logical_decl d) then ms 
 	else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end
       else ms
-  | (l,SEBmodule mb) :: msb -> 
+  | (l,SFBmodule mb) :: msb -> 
       let ms = extract_msb env mp all msb in
       let mp = MPdot (mp,l) in 
       if all || Visit.needed_mp mp then 
 	(l,SEmodule (extract_module env mp true mb)) :: ms
       else ms
-  | (l,SEBmodtype mtb) :: msb ->
+  | (l,SFBmodtype mtb) :: msb ->
       let ms = extract_msb env mp all msb in
-      let kn = make_kn mp empty_dirpath l in
-      if all || Visit.needed_kn kn then 
+      let mp = MPdot (mp,l) in
+       if all || Visit.needed_mp mp then 
 	(l,SEmodtype (extract_mtb env mtb)) :: ms
       else ms
 
 and extract_meb env mpo all = function 
-  | MEBident mp -> 
+  | SEBident mp ->  
       if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false; 
       Visit.add_mp mp; MEident mp 
-  | MEBapply (meb, meb',_) -> 
+  | SEBapply (meb, meb',_) -> 
       MEapply (extract_meb env None true meb, 
 	       extract_meb env None true meb')
-  | MEBfunctor (mbid, mtb, meb) -> 
+  | SEBfunctor (mbid, mtb, meb) -> 
       let mp = MPbound mbid in 
       let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in 
       MEfunctor (mbid, extract_mtb env mtb, 
 		 extract_meb env' None true meb)
-  | MEBstruct (msid, msb) -> 
+  | SEBstruct (msid, msb) -> 
       let mp,msb = match mpo with 
 	| None -> MPself msid, msb 
 	| Some mp -> mp, subst_msb (map_msid msid mp) msb
       in 
       let env' = add_structure mp msb env in 
       MEstruct (msid, extract_msb env' mp all msb) 
+  | SEBwith (_,_) -> anomaly "Not avaible yet"
 
 and extract_module env mp all mb = 
   (* [mb.mod_expr <> None ], since we look at modules from outside. *)
   (* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *)
   let meb = Option.get mb.mod_expr in
-  let mtb = match mb.mod_user_type with None -> mb.mod_type | Some mt -> mt in
+  let mtb = match mb.mod_type with None -> (Modops.type_of_mb env mb) | Some mt -> mt in
   (* Because of the "with" construct, the module type can be [MTBsig] with *)
   (* a msid different from the one of the module. Here is the patch. *)
-  let mtb = replicate_msid meb mtb in
+  let mtb = replicate_msid meb mtb in 
   { ml_mod_expr = extract_meb env (Some mp) all meb;
     ml_mod_type = extract_mtb env mtb }
 
+
 let unpack = function MEstruct (_,sel) -> sel | _ -> assert false 
 
 let mono_environment refs mpl = 
@@ -446,8 +465,3 @@ let extraction_library is_rec m =
   in 
   print struc; 
   reset ()
-
-
-
-
-
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 27687ae1c..b7be86bff 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -876,6 +876,20 @@ let extract_constant_spec env kn cb =
 	let t = snd (record_constant_type env kn (Some typ)) in 
 	Sval (r, type_expunge env t)
 
+let extract_with_type env cb = 
+  let typ = Typeops.type_of_constant_type env cb.const_type in 
+  match flag_of_type env typ with 
+    | (_ , Default) -> None
+    | (Logic, TypeScheme) ->Some ([],Tdummy Ktype)
+    | (Info, TypeScheme) -> 
+	let s,vl = type_sign_vl env typ in 
+	  (match cb.const_body with 
+	  | None -> assert false
+	  | Some body -> 
+	      let db = db_from_sign s in 
+	      let t = extract_type_scheme env db (force body) (List.length s)
+	      in Some ( vl, t) )
+		   
 let extract_inductive env kn = 
   let ind = extract_ind env kn in 
   add_recursors env kn; 
@@ -903,9 +917,3 @@ let logical_spec = function
   | Sval (_,Tdummy _) -> true
   | Sind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
   | _ -> false
-
-  
-
-
-
-
diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli
index cb0600d05..343d2b69a 100644
--- a/contrib/extraction/extraction.mli
+++ b/contrib/extraction/extraction.mli
@@ -21,6 +21,8 @@ val extract_constant : env -> constant -> constant_body -> ml_decl
 
 val extract_constant_spec : env -> constant -> constant_body -> ml_spec
 
+val extract_with_type : env -> constant_body -> ( identifier list * ml_type ) option
+
 val extract_fixpoint : 
   env -> constant array -> (constr, types) prec_declaration -> ml_decl 
 
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index ef963cc90..3add72d8b 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -126,9 +126,14 @@ type ml_specif =
   | Smodtype of ml_module_type
 
 and ml_module_type = 
-  | MTident of kernel_name
+  | MTident of module_path
   | MTfunsig of mod_bound_id * ml_module_type * ml_module_type
   | MTsig of mod_self_id * ml_module_sig
+  | MTwith of ml_module_type * ml_with_declaration
+
+and ml_with_declaration =  
+  | ML_With_type of identifier list * identifier list * ml_type
+  | ML_With_module of identifier list * module_path
 
 and ml_module_sig = (label * ml_specif) list
 
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index 79ba0ebc5..5c3f84822 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -28,49 +28,52 @@ let add_structure mp msb env =
     let kn = make_kn mp empty_dirpath l in 
     let con = make_con mp empty_dirpath l in 
     match elem with 
-      | SEBconst cb -> Environ.add_constant con cb env 
-      | SEBmind mib -> Environ.add_mind kn mib env 
-      | SEBmodule mb -> Modops.add_module (MPdot (mp,l)) mb env 
-      | SEBmodtype mtb -> Environ.add_modtype kn mtb env  
+      | SFBconst cb -> Environ.add_constant con cb env 
+      | SFBmind mib -> Environ.add_mind kn mib env 
+      | SFBmodule mb -> Modops.add_module (MPdot (mp,l)) mb env 
+      | SFBmodtype mtb -> Environ.add_modtype (MPdot (mp,l)) (mtb,None) env  
   in List.fold_left add_one env msb
 
 (*s Apply a module path substitution on a module.
    Build on the [Modops.subst_modtype] model. *)
 
 let rec subst_module sub mb =
-  let mtb' = Modops.subst_modtype sub mb.mod_type
+  let mtb' = Option.smartmap (Modops.subst_modtype sub) mb.mod_type
   and meb' = Option.smartmap (subst_meb sub) mb.mod_expr
-  and mtb'' = Option.smartmap (Modops.subst_modtype sub) mb.mod_user_type
   and mpo' = Option.smartmap (subst_mp sub) mb.mod_equiv in
-  if (mtb'==mb.mod_type) && (meb'==mb.mod_expr) && 
-    (mtb''==mb.mod_user_type) && (mpo'==mb.mod_equiv)
+  if (mtb'==mb.mod_type) && (meb'==mb.mod_expr) && (mpo'==mb.mod_equiv)
   then mb
   else { mod_expr= meb'; 
 	 mod_type=mtb'; 
-	 mod_user_type=mtb''; 
 	 mod_equiv=mpo'; 
 	 mod_constraints=mb.mod_constraints;
          mod_retroknowledge=[] } (* spiwack: since I'm lazy and it's unused at 
 				    this point. I forget about retroknowledge, 
-				    this may need a change later *)
+				    this may need a change later *) 
 
 and subst_meb sub = function 
-  | MEBident mp -> MEBident (subst_mp sub mp) 
-  | MEBfunctor (mbid, mtb, meb) -> 
+  | SEBident mp -> SEBident (subst_mp sub mp) 
+  | SEBfunctor (mbid, mtb, meb) -> 
       assert (not (occur_mbid mbid sub)); 
-      MEBfunctor (mbid, Modops.subst_modtype sub mtb, subst_meb sub meb)
-  | MEBstruct (msid, msb) -> 
+      SEBfunctor (mbid, Modops.subst_modtype sub mtb, subst_meb sub meb)
+  | SEBstruct (msid, msb) -> 
       assert (not (occur_msid msid sub));
-      MEBstruct (msid, subst_msb sub msb)
-  | MEBapply (meb, meb', c) -> 
-      MEBapply (subst_meb sub meb, subst_meb sub meb', c)
+      SEBstruct (msid, subst_msb sub msb)
+  | SEBapply (meb, meb', c) -> 
+      SEBapply (subst_meb sub meb, subst_meb sub meb', c)
+  | SEBwith (meb,With_module_body(id,mp,cst))->
+	SEBwith(subst_meb sub meb,
+		With_module_body(id,Mod_subst.subst_mp sub mp,cst))
+  | SEBwith (meb,With_definition_body(id,cb))->
+      SEBwith(subst_meb sub meb,
+	      With_definition_body(id,Declarations.subst_const_body sub cb))
 
 and subst_msb sub msb = 
   let subst_body = function
-    | SEBconst cb -> SEBconst (subst_const_body sub cb)
-    | SEBmind mib -> SEBmind (subst_mind sub mib)
-    | SEBmodule mb -> SEBmodule (subst_module sub mb)
-    | SEBmodtype mtb -> SEBmodtype (Modops.subst_modtype sub mtb)
+    | SFBconst cb -> SFBconst (subst_const_body sub cb)
+    | SFBmind mib -> SFBmind (subst_mind sub mib)
+    | SFBmodule mb -> SFBmodule (subst_module sub mb)
+    | SFBmodtype mtb -> SFBmodtype (Modops.subst_modtype sub mtb)
   in List.map (fun (l,b) -> (l,subst_body b)) msb
 
 (*s Change a msid in a module type, to follow a module expr. 
@@ -78,16 +81,29 @@ and subst_msb sub msb =
   [MTBsig] with a msid different from the one of the module. *)
 
 let rec replicate_msid meb mtb = match meb,mtb with 
-  | MEBfunctor (_, _, meb), MTBfunsig (mbid, mtb1, mtb2) -> 
+  | SEBfunctor (_, _, meb), SEBfunctor (mbid, mtb1, mtb2) -> 
       let mtb' = replicate_msid meb mtb2 in 
-      if mtb' == mtb2 then mtb else MTBfunsig (mbid, mtb1, mtb')
-  | MEBstruct (msid, _), MTBsig (msid1, msig) when msid <> msid1 -> 
+      if mtb' == mtb2 then mtb else SEBfunctor (mbid, mtb1, mtb')
+  | SEBstruct (msid, _), SEBstruct (msid1, msig) when msid <> msid1 -> 
       let msig' = Modops.subst_signature_msid msid1 (MPself msid) msig in
-      if msig' == msig then MTBsig (msid, msig) else MTBsig (msid, msig')
+      if msig' == msig then SEBstruct (msid, msig) else SEBstruct (msid, msig')
   | _ -> mtb
 
 (*S Functions upon ML modules. *)
-
+let rec  msid_of_mt = function
+  | MTident mp -> begin
+      match Modops.eval_struct (Global.env()) (SEBident mp) with
+	| SEBstruct(msid,_) -> MPself msid
+	| _ -> anomaly "Extraction:the With can'tbe applied to a funsig"
+    end
+  | MTwith(mt,_)-> msid_of_mt mt
+  | _ -> anomaly "Extraction:the With operator isn't applied to a name"
+      
+let  make_mp_with mp idl =
+  let idl_rev = List.rev idl in
+  let idl' = List.rev (List.tl idl_rev) in
+    (List.fold_left (fun mp id -> MPdot(mp,label_of_id id))
+       mp idl')
 (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a 
    [ml_structure]. *) 
 
@@ -95,6 +111,16 @@ let struct_iter do_decl do_spec s =
   let rec mt_iter = function 
     | MTident _ -> () 
     | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt'
+    | MTwith (mt,ML_With_type(idl,l,t))->
+	let mp_mt = msid_of_mt mt in
+      let mp = make_mp_with mp_mt idl in
+      let gr = ConstRef (
+	(make_con mp empty_dirpath
+	  (label_of_id ( 
+	    List.hd (List.rev idl))))) in
+	mt_iter mt;do_decl 
+	  (Dtype(gr,l,t))
+    | MTwith (mt,_)->mt_iter mt
     | MTsig (_, sign) -> List.iter spec_iter sign
   and spec_iter = function 
     | (_,Spec s) -> do_spec s
diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli
index c89590daa..8d0f3e923 100644
--- a/contrib/extraction/modutil.mli
+++ b/contrib/extraction/modutil.mli
@@ -20,18 +20,18 @@ open Mod_subst
 (* Add _all_ direct subobjects of a module, not only those exported. 
    Build on the [Modops.add_signature] model. *)
 
-val add_structure : module_path -> module_structure_body -> env -> env 
+val add_structure : module_path -> structure_body -> env -> env 
 
 (* Apply a module path substitution on a module.
    Build on the [Modops.subst_modtype] model. *)
 
 val subst_module : substitution -> module_body -> module_body 
-val subst_meb : substitution -> module_expr_body -> module_expr_body
-val subst_msb : substitution -> module_structure_body -> module_structure_body
+val subst_meb : substitution -> struct_expr_body -> struct_expr_body
+val subst_msb : substitution -> structure_body -> structure_body
 
 (* Change a msid in a module type, to follow a module expr. *)
 
-val replicate_msid : module_expr_body -> module_type_body -> module_type_body
+val replicate_msid : struct_expr_body -> struct_expr_body -> struct_expr_body
 
 (*s Functions upon ML modules. *)
 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 1ed82090a..16859a9c1 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -20,6 +20,26 @@ open Miniml
 open Mlutil
 open Modutil
 open Common
+open Declarations
+
+
+(*s Some utility functions. *)
+
+let rec  msid_of_mt = function
+  | MTident mp -> begin
+      match Modops.eval_struct (Global.env()) (SEBident mp) with
+	| SEBstruct(msid,_) -> MPself msid
+	| _ -> anomaly "Extraction:the With can'tbe applied to a funsig"
+    end
+  | MTwith(mt,_)-> msid_of_mt mt
+  | _ -> anomaly "Extraction:the With operator isn't applied to a name"
+
+let  make_mp_with mp idl =
+  let idl_rev = List.rev idl in
+  let idl' = List.rev (List.tl idl_rev) in
+    (List.fold_left (fun mp id -> MPdot(mp,label_of_id id))
+       mp idl')
+
 
 let pp_tvar id = 
   let s = string_of_id id in 
@@ -585,7 +605,7 @@ let rec pp_specif = function
 
 and pp_module_type ol = function 
   | MTident kn -> 
-      let mp,_,l = repr_kn kn in pp_modname (MPdot (mp,l))
+      pp_modname kn
   | MTfunsig (mbid, mt, mt') -> 
       let name = pp_modname (MPbound mbid) in 
       let typ = pp_module_type None mt in 
@@ -600,10 +620,41 @@ and pp_module_type ol = function
       pop_visible (); 
       str "sig " ++ fnl () ++ 
       v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++
-      fnl () ++ str "end"
-
+	fnl () ++ str "end"
+  | MTwith(mt,ML_With_type(idl,vl,typ)) ->
+      let l = rename_tvars keywords vl in 
+      let ids = pp_parameters l in 
+      let mp_mt = msid_of_mt mt in
+      let mp = make_mp_with mp_mt idl in
+      let gr = ConstRef (
+	(make_con mp empty_dirpath
+	  (label_of_id ( 
+	    List.hd (List.rev idl))))) in
+	push_visible mp_mt;
+	let s = pp_module_type None mt ++
+	  str " with type " ++
+	  pp_global Type gr ++
+	  ids in
+	  pop_visible();
+	  s ++ str "=" ++ spc () ++
+	  pp_type false  vl typ
+  | MTwith(mt,ML_With_module(idl,mp)) ->
+      let mp_mt=msid_of_mt mt in
+	push_visible mp_mt;
+	let s = 
+	  pp_module_type None mt ++
+	    str " with module " ++
+	    (pp_modname
+	       (List.fold_left (fun mp id -> MPdot(mp,label_of_id id))
+		  mp_mt idl))
+	  ++ str " = "  
+	in
+	  pop_visible ();
+	  s ++ (pp_modname mp)
+	    
+	    
 let is_short = function MEident _ | MEapply _ -> true | _ -> false
-
+  
 let rec pp_structure_elem = function 
   | (l,SEdecl d) -> 
        (try